Anne is furry. Anne is kind. Dave is not kind. Dave is round. Dave is smart. Dave is not young. Fiona is big. Fiona is furry. Fiona is round. Fiona is smart. Gary is kind. Gary is smart. If something is cold and big then it is furry. All kind, cold things are smart. If something is furry then it is cold. Smart things are round. All round things are big. Kind, big things are young.
Anne is furry.
("Anne" "is" "furry" "+")
Anne is kind.
("Anne" "is" "kind" "+")
Dave is not kind.
("Dave" "is" "kind" "-")
Dave is round.
("Dave" "is" "round" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is not young.
("Dave" "is" "young" "-")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is furry.
("Fiona" "is" "furry" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is kind.
("Gary" "is" "kind" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is cold and big then it is furry.
((("something" "is" "cold" "+") ("something" "is" "big" "+")) -> ("something" "is" "furry" "+"))
All kind, cold things are smart.
((("something" "is" "kind" "+") ("something" "is" "cold" "+")) -> ("something" "is" "smart" "+"))
If something is furry then it is cold.
((("something" "is" "furry" "+")) -> ("something" "is" "cold" "+"))
Smart things are round.
((("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
All round things are big.
((("something" "is" "round" "+")) -> ("something" "is" "big" "+"))
Kind, big things are young.
((("something" "is" "kind" "+") ("something" "is" "big" "+")) -> ("something" "is" "young" "+"))
Gary is smart.
True
1
proof
[(triple12)]
("Gary" "is" "smart" "+")
triple12
Dave is not smart.
False
1
inv-proof
[(triple5)]
("Dave" "is" "smart" "-")
triple5
Dave is big.
True
2
proof
[(((triple4) -> rule5) OR ((((triple5) -> rule4)) -> rule5))]
("Dave" "is" "big" "+")
((triple4) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Anne is not cold.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "cold" "-")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Gary is big.
True
3
proof
[(((((triple12) -> rule4)) -> rule5))]
("Gary" "is" "big" "+")
((((triple12) -> (rule4 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Anne is not smart.
False
4
inv-proof
[(((triple2 ((triple1) -> rule3)) -> rule2))]
("Anne" "is" "smart" "-")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Gary is young.
True
5
proof
[(((triple11 ((((triple12) -> rule4)) -> rule5)) -> rule6))]
("Gary" "is" "young" "+")
((triple11 ((((triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is not young.
False
5
inv-proof
[(((triple11 ((((triple12) -> rule4)) -> rule5)) -> rule6))]
("Gary" "is" "young" "-")
((triple11 ((((triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Anne is big.
True
6
proof
[(((((((triple2 ((triple1) -> rule3)) -> rule2)) -> rule4)) -> rule5))]
("Anne" "is" "big" "+")
((((((triple2 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is not big.
False
6
inv-proof
[(((((((triple2 ((triple1) -> rule3)) -> rule2)) -> rule4)) -> rule5))]
("Anne" "is" "big" "-")
((((((triple2 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is young.
True
8
proof
[(((triple2 ((((((triple2 ((triple1) -> rule3)) -> rule2)) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "young" "+")
((triple2 ((((((triple2 ((triple1) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Anne is not young.
False
8
inv-proof
[(((triple2 ((((((triple2 ((triple1) -> rule3)) -> rule2)) -> rule4)) -> rule5)) -> rule6))]
("Anne" "is" "young" "-")
((triple2 ((((((triple2 ((triple1) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5
Dave is not furry.
Unknown
inv-rconc
[@2: Dave is furry.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Dave" "is" "furry" "-")
Gary is furry.
Unknown
rconc
[@2: Gary is furry.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Gary" "is" "furry" "+")
Gary is not cold.
Unknown
inv-rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Gary" "is" "cold" "-")
Fiona is young.
Unknown
rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Fiona" "is" "young" "+")
Dave is not cold.
Unknown
inv-rconc
[@2: Dave is cold.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Dave" "is" "cold" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Anne is furry.[(triple1)] Anne is kind.[(triple2)] Dave is not kind.[(triple3)] Dave is not young.[(triple6)] Dave is round.[(triple4 OR ((triple5) -> rule4))] Dave is smart.[(triple5)] Fiona is big.[(triple7 OR ((triple9) -> rule5) OR ((((triple10) -> rule4)) -> rule5))] Fiona is furry.[(triple8)] Fiona is round.[(triple9 OR ((triple10) -> rule4))] Fiona is smart.[(triple10)] Gary is kind.[(triple11)] Gary is smart.[(triple12)] @1: Anne is cold.[(((triple1) -> rule3))] Dave is big.[(((triple4) -> rule5) OR ((((triple5) -> rule4)) -> rule5))] Fiona is cold.[(((triple8) -> rule3))] Gary is round.[(((triple12) -> rule4))] @2: Anne is smart.[(((triple2 ((triple1) -> rule3)) -> rule2))] Gary is big.[(((((triple12) -> rule4)) -> rule5))] @3: Anne is round.[(((((triple2 ((triple1) -> rule3)) -> rule2)) -> rule4))] Gary is young.[(((triple11 ((((triple12) -> rule4)) -> rule5)) -> rule6))] @4: Anne is big.[(((((((triple2 ((triple1) -> rule3)) -> rule2)) -> rule4)) -> rule5))] @5: Anne is young.[(((triple2 ((((((triple2 ((triple1) -> rule3)) -> rule2)) -> rule4)) -> rule5)) -> rule6))]
Anne is furry.
("Anne" "is" "furry" "+")
triple1
Anne is kind.
("Anne" "is" "kind" "+")
triple2
Dave is not kind.
("Dave" "is" "kind" "-")
triple3
Dave is not young.
("Dave" "is" "young" "-")
triple6
Dave is round.
("Dave" "is" "round" "+")
triple4
((triple5) -> (rule4 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Fiona is big.
("Fiona" "is" "big" "+")
triple7
((triple9) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
int2
Fiona is furry.
("Fiona" "is" "furry" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
((triple10) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Gary is kind.
("Gary" "is" "kind" "+")
triple11
Gary is smart.
("Gary" "is" "smart" "+")
triple12
Anne is cold.
("Anne" "is" "cold" "+")
((triple1) -> (rule3 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((((triple5) -> (rule4 % int2))) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple8) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple12) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
((triple2 ((triple1) -> (rule3 % int2))) -> (rule2 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Gary is big.
("Gary" "is" "big" "+")
((((triple12) -> (rule4 % int2))) -> (rule5 % int1))
Gary is big.
("Gary" "is" "big" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((((triple2 ((triple1) -> (rule3 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Gary is young.
("Gary" "is" "young" "+")
((triple11 ((((triple12) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is big.
("Gary" "is" "big" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Anne is big.
("Anne" "is" "big" "+")
((((((triple2 ((triple1) -> (rule3 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is cold.
("Anne" "is" "cold" "+")
int4
Anne is young.
("Anne" "is" "young" "+")
((triple2 ((((((triple2 ((triple1) -> (rule3 % int5))) -> (rule2 % int4))) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4
Anne is cold.
("Anne" "is" "cold" "+")
int5