Anne is blue. Anne is red. Bob is quiet. Bob is red. Gary is blue. Gary is nice. Gary is quiet. Gary is red. Gary is smart. Gary is young. All round, blue things are young. If Bob is young then Bob is red. If something is young and blue then it is nice. Red, smart things are round. Smart things are quiet. All blue things are smart.
Anne is blue.
("Anne" "is" "blue" "+")
Anne is red.
("Anne" "is" "red" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Gary is blue.
("Gary" "is" "blue" "+")
Gary is nice.
("Gary" "is" "nice" "+")
Gary is quiet.
("Gary" "is" "quiet" "+")
Gary is red.
("Gary" "is" "red" "+")
Gary is smart.
("Gary" "is" "smart" "+")
Gary is young.
("Gary" "is" "young" "+")
All round, blue things are young.
((("something" "is" "round" "+") ("something" "is" "blue" "+")) -> ("something" "is" "young" "+"))
If Bob is young then Bob is red.
((("Bob" "is" "young" "+")) -> ("Bob" "is" "red" "+"))
If something is young and blue then it is nice.
((("something" "is" "young" "+") ("something" "is" "blue" "+")) -> ("something" "is" "nice" "+"))
Red, smart things are round.
((("something" "is" "red" "+") ("something" "is" "smart" "+")) -> ("something" "is" "round" "+"))
Smart things are quiet.
((("something" "is" "smart" "+")) -> ("something" "is" "quiet" "+"))
All blue things are smart.
((("something" "is" "blue" "+")) -> ("something" "is" "smart" "+"))
Gary is young.
True
1
proof
[(triple10 OR ((((triple8 triple9) -> rule4) triple5) -> rule1) OR ((((triple8 ((triple5) -> rule6)) -> rule4) triple5) -> rule1))]
("Gary" "is" "young" "+")
triple10
((((triple8 triple9) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple8 ((triple5) -> (rule6 % int3))) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Gary is not nice.
False
1
inv-proof
[(triple6 OR ((triple10 triple5) -> rule3) OR ((((((triple8 triple9) -> rule4) triple5) -> rule1) triple5) -> rule3) OR ((((((triple8 ((triple5) -> rule6)) -> rule4) triple5) -> rule1) triple5) -> rule3))]
("Gary" "is" "nice" "-")
triple6
((triple10 triple5) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((((triple8 triple9) -> (rule4 % int3)) triple5) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple8 ((triple5) -> (rule6 % int4))) -> (rule4 % int3)) triple5) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Anne is smart.
True
2
proof
[(((triple1) -> rule6))]
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is not round.
False
3
inv-proof
[(((triple8 triple9) -> rule4) OR ((triple8 ((triple5) -> rule6)) -> rule4))]
("Gary" "is" "round" "-")
((triple8 triple9) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple8 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is quiet.
True
3
proof
[(((((triple1) -> rule6)) -> rule5))]
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is not round.
False
4
inv-proof
[(((triple2 ((triple1) -> rule6)) -> rule4))]
("Anne" "is" "round" "-")
((triple2 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
True
6
proof
[(((((triple2 ((triple1) -> rule6)) -> rule4) triple1) -> rule1))]
("Anne" "is" "young" "+")
((((triple2 ((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is not young.
False
6
inv-proof
[(((((triple2 ((triple1) -> rule6)) -> rule4) triple1) -> rule1))]
("Anne" "is" "young" "-")
((((triple2 ((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Bob is not young.
Unknown
inv-rconc
[@1: Bob is young.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "young" "-")
Bob is nice.
Unknown
rconc
[@1: Bob is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Bob" "is" "nice" "+")
Bob is not round.
Unknown
inv-rconc
[@2: Bob is round.[CWA. Example of deepest failure = (rule4 <- rule6 <- FAIL)]]
("Bob" "is" "round" "-")
Bob is smart.
Unknown
rconc
[@1: Bob is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Bob" "is" "smart" "+")
@0: Anne is blue.[(triple1)] Anne is red.[(triple2)] Bob is quiet.[(triple3)] Bob is red.[(triple4)] Gary is blue.[(triple5)] Gary is nice.[(triple6 OR ((triple10 triple5) -> rule3) OR ((((((triple8 triple9) -> rule4) triple5) -> rule1) triple5) -> rule3) OR ((((((triple8 ((triple5) -> rule6)) -> rule4) triple5) -> rule1) triple5) -> rule3))] Gary is quiet.[(triple7 OR ((triple9) -> rule5) OR ((((triple5) -> rule6)) -> rule5))] Gary is red.[(triple8)] Gary is smart.[(triple9 OR ((triple5) -> rule6))] Gary is young.[(triple10 OR ((((triple8 triple9) -> rule4) triple5) -> rule1) OR ((((triple8 ((triple5) -> rule6)) -> rule4) triple5) -> rule1))] @1: Anne is smart.[(((triple1) -> rule6))] Gary is round.[(((triple8 triple9) -> rule4) OR ((triple8 ((triple5) -> rule6)) -> rule4))] @2: Anne is quiet.[(((((triple1) -> rule6)) -> rule5))] Anne is round.[(((triple2 ((triple1) -> rule6)) -> rule4))] @3: Anne is young.[(((((triple2 ((triple1) -> rule6)) -> rule4) triple1) -> rule1))] @4: Anne is nice.[(((((((triple2 ((triple1) -> rule6)) -> rule4) triple1) -> rule1) triple1) -> rule3))]
Anne is blue.
("Anne" "is" "blue" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Bob is quiet.
("Bob" "is" "quiet" "+")
triple3
Bob is red.
("Bob" "is" "red" "+")
triple4
Gary is blue.
("Gary" "is" "blue" "+")
triple5
Gary is nice.
("Gary" "is" "nice" "+")
triple6
((triple10 triple5) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
((((((triple8 triple9) -> (rule4 % int3)) triple5) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
((((((triple8 ((triple5) -> (rule6 % int4))) -> (rule4 % int3)) triple5) -> (rule1 % int2)) triple5) -> (rule3 % int1))
Gary is nice.
("Gary" "is" "nice" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
int2
Gary is round.
("Gary" "is" "round" "+")
int3
Gary is smart.
("Gary" "is" "smart" "+")
int4
Gary is quiet.
("Gary" "is" "quiet" "+")
triple7
((triple9) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
((((triple5) -> (rule6 % int2))) -> (rule5 % int1))
Gary is quiet.
("Gary" "is" "quiet" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Gary is red.
("Gary" "is" "red" "+")
triple8
Gary is smart.
("Gary" "is" "smart" "+")
triple9
((triple5) -> (rule6 % int1))
Gary is smart.
("Gary" "is" "smart" "+")
int1
Gary is young.
("Gary" "is" "young" "+")
triple10
((((triple8 triple9) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
((((triple8 ((triple5) -> (rule6 % int3))) -> (rule4 % int2)) triple5) -> (rule1 % int1))
Gary is young.
("Gary" "is" "young" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
int2
Gary is smart.
("Gary" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple1) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Gary is round.
("Gary" "is" "round" "+")
((triple8 triple9) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
((triple8 ((triple5) -> (rule6 % int2))) -> (rule4 % int1))
Gary is round.
("Gary" "is" "round" "+")
int1
Gary is smart.
("Gary" "is" "smart" "+")
int2
Anne is quiet.
("Anne" "is" "quiet" "+")
((((triple1) -> (rule6 % int2))) -> (rule5 % int1))
Anne is quiet.
("Anne" "is" "quiet" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
((triple2 ((triple1) -> (rule6 % int2))) -> (rule4 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((triple2 ((triple1) -> (rule6 % int3))) -> (rule4 % int2)) triple1) -> (rule1 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is round.
("Anne" "is" "round" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is nice.
("Anne" "is" "nice" "+")
((((((triple2 ((triple1) -> (rule6 % int4))) -> (rule4 % int3)) triple1) -> (rule1 % int2)) triple1) -> (rule3 % int1))
Anne is nice.
("Anne" "is" "nice" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is round.
("Anne" "is" "round" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4