Charlie is big. Charlie is blue. Charlie is red. Charlie is rough. Charlie is round. Charlie is not white. Charlie is not young. Dave is big. Dave is blue. Dave is not young. Harry is big. Harry is blue. Harry is not red. Harry is rough. Harry is young. All blue, white things are round. Young things are white.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is not white.
("Charlie" "is" "white" "-")
Charlie is not young.
("Charlie" "is" "young" "-")
Dave is big.
("Dave" "is" "big" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is not young.
("Dave" "is" "young" "-")
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is not red.
("Harry" "is" "red" "-")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is young.
("Harry" "is" "young" "+")
All blue, white things are round.
((("something" "is" "blue" "+") ("something" "is" "white" "+")) -> ("something" "is" "round" "+"))
Young things are white.
((("something" "is" "young" "+")) -> ("something" "is" "white" "+"))
Dave is not young.
True
1
proof
[(triple10)]
("Dave" "is" "young" "-")
triple10
Harry is not blue.
False
1
inv-proof
[(triple12)]
("Harry" "is" "blue" "-")
triple12
Harry is white.
True
2
proof
[(((triple15) -> rule2))]
("Harry" "is" "white" "+")
((triple15) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is not white.
False
2
inv-proof
[(((triple15) -> rule2))]
("Harry" "is" "white" "-")
((triple15) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
True
4
proof
[(((triple12 ((triple15) -> rule2)) -> rule1))]
("Harry" "is" "round" "+")
((triple12 ((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is not round.
False
4
inv-proof
[(((triple12 ((triple15) -> rule2)) -> rule1))]
("Harry" "is" "round" "-")
((triple12 ((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Dave is not white.
Unknown
inv-rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "-")
Dave is round.
Unknown
rconc
[@2: Dave is round.[CWA. Example of deepest failure = (rule1 <- rule2 <- FAIL)]]
("Dave" "is" "round" "+")
Dave is not rough.
Unknown
inv-random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "-")
Dave is red.
Unknown
random
[@0: Dave is red.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "red" "+")
@0: Charlie is big.[(triple1)] Charlie is blue.[(triple2)] Charlie is not white.[(triple6)] Charlie is not young.[(triple7)] Charlie is red.[(triple3)] Charlie is rough.[(triple4)] Charlie is round.[(triple5)] Dave is big.[(triple8)] Dave is blue.[(triple9)] Dave is not young.[(triple10)] Harry is big.[(triple11)] Harry is blue.[(triple12)] Harry is not red.[(triple13)] Harry is rough.[(triple14)] Harry is young.[(triple15)] @1: Harry is white.[(((triple15) -> rule2))] @2: Harry is round.[(((triple12 ((triple15) -> rule2)) -> rule1))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is blue.
("Charlie" "is" "blue" "+")
triple2
Charlie is not white.
("Charlie" "is" "white" "-")
triple6
Charlie is not young.
("Charlie" "is" "young" "-")
triple7
Charlie is red.
("Charlie" "is" "red" "+")
triple3
Charlie is rough.
("Charlie" "is" "rough" "+")
triple4
Charlie is round.
("Charlie" "is" "round" "+")
triple5
Dave is big.
("Dave" "is" "big" "+")
triple8
Dave is blue.
("Dave" "is" "blue" "+")
triple9
Dave is not young.
("Dave" "is" "young" "-")
triple10
Harry is big.
("Harry" "is" "big" "+")
triple11
Harry is blue.
("Harry" "is" "blue" "+")
triple12
Harry is not red.
("Harry" "is" "red" "-")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is young.
("Harry" "is" "young" "+")
triple15
Harry is white.
("Harry" "is" "white" "+")
((triple15) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
((triple12 ((triple15) -> (rule2 % int2))) -> (rule1 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2