Anne is red. Anne is round. Anne is young. Charlie is kind. Charlie is smart. Charlie is young. Dave is kind. Dave is quiet. Dave is red. Dave is smart. Red people are round. If Anne is young then Anne is big. Smart people are red. All kind, red people are quiet. All quiet, smart people are young. All smart people are young.
Anne is red.
("Anne" "is" "red" "+")
Anne is round.
("Anne" "is" "round" "+")
Anne is young.
("Anne" "is" "young" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
Dave is red.
("Dave" "is" "red" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Red people are round.
((("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
If Anne is young then Anne is big.
((("Anne" "is" "young" "+")) -> ("Anne" "is" "big" "+"))
Smart people are red.
((("someone" "is" "smart" "+")) -> ("someone" "is" "red" "+"))
All kind, red people are quiet.
((("someone" "is" "kind" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
All quiet, smart people are young.
((("someone" "is" "quiet" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
All smart people are young.
((("someone" "is" "smart" "+")) -> ("someone" "is" "young" "+"))
Dave is red.
True
1
proof
[(triple9 OR ((triple10) -> rule3))]
("Dave" "is" "red" "+")
triple9
((triple10) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Charlie is not young.
False
1
inv-proof
[(triple6 OR ((triple5) -> rule6) OR ((((triple4 ((triple5) -> rule3)) -> rule4) triple5) -> rule5))]
("Charlie" "is" "young" "-")
triple6
((triple5) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple4 ((triple5) -> (rule3 % int3))) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Anne is not quiet.
Unknown
inv-rconc
[@1: Anne is quiet.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Anne" "is" "quiet" "-")
Charlie is big.
Unknown
random
[@0: Charlie is big.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "big" "+")
@0: Anne is red.[(triple1)] Anne is round.[(triple2 OR ((triple1) -> rule1))] Anne is young.[(triple3)] Charlie is kind.[(triple4)] Charlie is smart.[(triple5)] Charlie is young.[(triple6 OR ((triple5) -> rule6) OR ((((triple4 ((triple5) -> rule3)) -> rule4) triple5) -> rule5))] Dave is kind.[(triple7)] Dave is quiet.[(triple8 OR ((triple7 triple9) -> rule4) OR ((triple7 ((triple10) -> rule3)) -> rule4))] Dave is red.[(triple9 OR ((triple10) -> rule3))] Dave is smart.[(triple10)] @1: Anne is big.[(((triple3) -> rule2))] Charlie is red.[(((triple5) -> rule3))] Dave is round.[(((triple9) -> rule1) OR ((((triple10) -> rule3)) -> rule1))] Dave is young.[(((triple10) -> rule6) OR ((triple8 triple10) -> rule5) OR ((((triple7 triple9) -> rule4) triple10) -> rule5) OR ((((triple7 ((triple10) -> rule3)) -> rule4) triple10) -> rule5))] @2: Charlie is quiet.[(((triple4 ((triple5) -> rule3)) -> rule4))] Charlie is round.[(((((triple5) -> rule3)) -> rule1))]
Anne is red.
("Anne" "is" "red" "+")
triple1
Anne is round.
("Anne" "is" "round" "+")
triple2
((triple1) -> (rule1 % int1))
Anne is round.
("Anne" "is" "round" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
triple3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple4
Charlie is smart.
("Charlie" "is" "smart" "+")
triple5
Charlie is young.
("Charlie" "is" "young" "+")
triple6
((triple5) -> (rule6 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
((((triple4 ((triple5) -> (rule3 % int3))) -> (rule4 % int2)) triple5) -> (rule5 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Dave is kind.
("Dave" "is" "kind" "+")
triple7
Dave is quiet.
("Dave" "is" "quiet" "+")
triple8
((triple7 triple9) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
((triple7 ((triple10) -> (rule3 % int2))) -> (rule4 % int1))
Dave is quiet.
("Dave" "is" "quiet" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
triple9
((triple10) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is smart.
("Dave" "is" "smart" "+")
triple10
Anne is big.
("Anne" "is" "big" "+")
((triple3) -> (rule2 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple5) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple9) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is young.
("Dave" "is" "young" "+")
((triple10) -> (rule6 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((triple8 triple10) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
((((triple7 triple9) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
((((triple7 ((triple10) -> (rule3 % int3))) -> (rule4 % int2)) triple10) -> (rule5 % int1))
Dave is young.
("Dave" "is" "young" "+")
int1
Dave is quiet.
("Dave" "is" "quiet" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
int3
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((triple4 ((triple5) -> (rule3 % int2))) -> (rule4 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is round.
("Charlie" "is" "round" "+")
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is round.
("Charlie" "is" "round" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2