Charlie is green. Charlie is quiet. Charlie is round. Charlie is smart. Dave is smart. Dave is white. Fiona is green. Fiona is red. Fiona is round. Fiona is smart. Fiona is white. Fiona is young. Red, round people are green. If someone is smart then they are white. If Dave is smart and Dave is white then Dave is round.
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is quiet.
("Charlie" "is" "quiet" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is smart.
("Charlie" "is" "smart" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Dave is white.
("Dave" "is" "white" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Red, round people are green.
((("someone" "is" "red" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "green" "+"))
If someone is smart then they are white.
((("someone" "is" "smart" "+")) -> ("someone" "is" "white" "+"))
If Dave is smart and Dave is white then Dave is round.
((("Dave" "is" "smart" "+") ("Dave" "is" "white" "+")) -> ("Dave" "is" "round" "+"))
Fiona is young.
True
1
proof
[(triple12)]
("Fiona" "is" "young" "+")
triple12
Fiona is not young.
False
1
inv-proof
[(triple12)]
("Fiona" "is" "young" "-")
triple12
Charlie is white.
True
2
proof
[(((triple4) -> rule2))]
("Charlie" "is" "white" "+")
((triple4) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is not round.
False
3
inv-proof
[(((triple5 triple6) -> rule3) OR ((triple5 ((triple5) -> rule2)) -> rule3))]
("Dave" "is" "round" "-")
((triple5 triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2
Dave is not green.
Unknown
inv-rconc
[@1: Dave is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "green" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Charlie is not young.
Unknown
inv-random
[@0: Charlie is young.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "young" "-")
Fiona is quiet.
Unknown
random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "+")
@0: Charlie is green.[(triple1)] Charlie is quiet.[(triple2)] Charlie is round.[(triple3)] Charlie is smart.[(triple4)] Dave is smart.[(triple5)] Dave is white.[(triple6 OR ((triple5) -> rule2))] Fiona is green.[(triple7 OR ((triple8 triple9) -> rule1))] Fiona is red.[(triple8)] Fiona is round.[(triple9)] Fiona is smart.[(triple10)] Fiona is white.[(triple11 OR ((triple10) -> rule2))] Fiona is young.[(triple12)] @1: Charlie is white.[(((triple4) -> rule2))] Dave is round.[(((triple5 triple6) -> rule3) OR ((triple5 ((triple5) -> rule2)) -> rule3))]
Charlie is green.
("Charlie" "is" "green" "+")
triple1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
triple2
Charlie is round.
("Charlie" "is" "round" "+")
triple3
Charlie is smart.
("Charlie" "is" "smart" "+")
triple4
Dave is smart.
("Dave" "is" "smart" "+")
triple5
Dave is white.
("Dave" "is" "white" "+")
triple6
((triple5) -> (rule2 % int1))
Dave is white.
("Dave" "is" "white" "+")
int1
Fiona is green.
("Fiona" "is" "green" "+")
triple7
((triple8 triple9) -> (rule1 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple8
Fiona is round.
("Fiona" "is" "round" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
Fiona is white.
("Fiona" "is" "white" "+")
triple11
((triple10) -> (rule2 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple12
Charlie is white.
("Charlie" "is" "white" "+")
((triple4) -> (rule2 % int1))
Charlie is white.
("Charlie" "is" "white" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple5 triple6) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
((triple5 ((triple5) -> (rule2 % int2))) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Dave is white.
("Dave" "is" "white" "+")
int2