Charlie is big. Charlie is kind. Charlie is rough. Dave is blue. Dave is cold. Dave is not furry. Dave is not rough. Furry, kind things are rough. Blue, big things are not white. If something is furry then it is white. Big things are kind. Blue things are big. If something is blue then it is big. If Dave is rough then Dave is white. If Dave is furry and Dave is kind then Dave is not blue.
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is blue.
("Dave" "is" "blue" "+")
Dave is cold.
("Dave" "is" "cold" "+")
Dave is not furry.
("Dave" "is" "furry" "-")
Dave is not rough.
("Dave" "is" "rough" "-")
Furry, kind things are rough.
((("something" "is" "furry" "+") ("something" "is" "kind" "+")) -> ("something" "is" "rough" "+"))
Blue, big things are not white.
((("something" "is" "blue" "+") ("something" "is" "big" "+")) -> ("something" "is" "white" "-"))
If something is furry then it is white.
((("something" "is" "furry" "+")) -> ("something" "is" "white" "+"))
Big things are kind.
((("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Blue things are big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
If Dave is rough then Dave is white.
((("Dave" "is" "rough" "+")) -> ("Dave" "is" "white" "+"))
If Dave is furry and Dave is kind then Dave is not blue.
((("Dave" "is" "furry" "+") ("Dave" "is" "kind" "+")) -> ("Dave" "is" "blue" "-"))
Dave is blue.
True
1
proof
[(triple4)]
("Dave" "is" "blue" "+")
triple4
Charlie is not kind.
False
1
inv-proof
[(triple2 OR ((triple1) -> rule4))]
("Charlie" "is" "kind" "-")
triple2
((triple1) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Dave is big.
True
2
proof
[(((triple4) -> rule5) OR ((triple4) -> rule6))]
("Dave" "is" "big" "+")
((triple4) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple4) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple4) -> rule5) OR ((triple4) -> rule6))]
("Dave" "is" "big" "-")
((triple4) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple4) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
True
3
proof
[(((((triple4) -> rule5)) -> rule4) OR ((((triple4) -> rule6)) -> rule4))]
("Dave" "is" "kind" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is white.
False
4
inv-proof
[(((triple4 ((triple4) -> rule5)) -> rule2) OR ((triple4 ((triple4) -> rule6)) -> rule2))]
("Dave" "is" "white" "+")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple4 ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is not white.
Unknown
inv-rconc
[@1: Charlie is white.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "white" "-")
Charlie is blue.
Unknown
random
[@0: Charlie is blue.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "blue" "+")
Charlie is not furry.
Unknown
inv-random
[@0: Charlie is furry.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "furry" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Charlie is big.[(triple1)] Charlie is kind.[(triple2 OR ((triple1) -> rule4))] Charlie is rough.[(triple3)] Dave is blue.[(triple4)] Dave is cold.[(triple5)] Dave is not furry.[(triple6)] Dave is not rough.[(triple7)] @1: Dave is big.[(((triple4) -> rule5) OR ((triple4) -> rule6))] @2: Dave is kind.[(((((triple4) -> rule5)) -> rule4) OR ((((triple4) -> rule6)) -> rule4))] Dave is not white.[(((triple4 ((triple4) -> rule5)) -> rule2) OR ((triple4 ((triple4) -> rule6)) -> rule2))]
Charlie is big.
("Charlie" "is" "big" "+")
triple1
Charlie is kind.
("Charlie" "is" "kind" "+")
triple2
((triple1) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
triple3
Dave is blue.
("Dave" "is" "blue" "+")
triple4
Dave is cold.
("Dave" "is" "cold" "+")
triple5
Dave is not furry.
("Dave" "is" "furry" "-")
triple6
Dave is not rough.
("Dave" "is" "rough" "-")
triple7
Dave is big.
("Dave" "is" "big" "+")
((triple4) -> (rule5 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
((triple4) -> (rule6 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is kind.
("Dave" "is" "kind" "+")
((((triple4) -> (rule5 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((((triple4) -> (rule6 % int2))) -> (rule4 % int1))
Dave is kind.
("Dave" "is" "kind" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is not white.
("Dave" "is" "white" "-")
((triple4 ((triple4) -> (rule5 % int2))) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
((triple4 ((triple4) -> (rule6 % int2))) -> (rule2 % int1))
Dave is not white.
("Dave" "is" "white" "-")
int1
Dave is big.
("Dave" "is" "big" "+")
int2