Charlie is rough. Dave is quiet. All rough things are big. All quiet things are big. If something is furry and not rough then it is cold. All quiet, red things are furry. All big things are red. If something is furry and not rough then it is not red. All cold things are red. All red things are quiet.
Charlie is rough.
("Charlie" "is" "rough" "+")
Dave is quiet.
("Dave" "is" "quiet" "+")
All rough things are big.
((("something" "is" "rough" "+")) -> ("something" "is" "big" "+"))
All quiet things are big.
((("something" "is" "quiet" "+")) -> ("something" "is" "big" "+"))
If something is furry and not rough then it is cold.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "cold" "+"))
All quiet, red things are furry.
((("something" "is" "quiet" "+") ("something" "is" "red" "+")) -> ("something" "is" "furry" "+"))
All big things are red.
((("something" "is" "big" "+")) -> ("something" "is" "red" "+"))
If something is furry and not rough then it is not red.
((("something" "is" "furry" "+") ("something" "is" "rough" "~")) -> ("something" "is" "red" "-"))
All cold things are red.
((("something" "is" "cold" "+")) -> ("something" "is" "red" "+"))
All red things are quiet.
((("something" "is" "red" "+")) -> ("something" "is" "quiet" "+"))
Dave is quiet.
True
1
proof
[(triple2)]
("Dave" "is" "quiet" "+")
triple2
Charlie is not rough.
False
1
inv-proof
[(triple1)]
("Charlie" "is" "rough" "-")
triple1
Charlie is big.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is not big.
False
2
inv-proof
[(((triple2) -> rule2))]
("Dave" "is" "big" "-")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Charlie is red.
True
3
proof
[(((((triple1) -> rule1)) -> rule5))]
("Charlie" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule5))]
("Charlie" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Charlie is quiet.
True
4
proof
[(((((((triple1) -> rule1)) -> rule5)) -> rule8))]
("Charlie" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Dave is not furry.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule4))]
("Dave" "is" "furry" "-")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Charlie is not cold.
Unknown
inv-rconc
[@1: Charlie is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Charlie" "is" "cold" "-")
Dave is cold.
Unknown
rconc
[@1: Dave is cold.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Dave" "is" "cold" "+")
Dave is not kind.
Unknown
inv-random
[@0: Dave is kind.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "kind" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Charlie is rough.[(triple1)] Dave is quiet.[(triple2)] @1: Charlie is big.[(((triple1) -> rule1))] Dave is big.[(((triple2) -> rule2))] @2: Charlie is red.[(((((triple1) -> rule1)) -> rule5))] Dave is red.[(((((triple2) -> rule2)) -> rule5))] @3: Charlie is quiet.[(((((((triple1) -> rule1)) -> rule5)) -> rule8))] Dave is furry.[(((triple2 ((((triple2) -> rule2)) -> rule5)) -> rule4))] @4: Charlie is furry.[(((((((((triple1) -> rule1)) -> rule5)) -> rule8) ((((triple1) -> rule1)) -> rule5)) -> rule4))]
Charlie is rough.
("Charlie" "is" "rough" "+")
triple1
Dave is quiet.
("Dave" "is" "quiet" "+")
triple2
Charlie is big.
("Charlie" "is" "big" "+")
((triple1) -> (rule1 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((triple2) -> (rule2 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule5 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule2 % int2))) -> (rule5 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Charlie is quiet.
("Charlie" "is" "quiet" "+")
((((((triple1) -> (rule1 % int3))) -> (rule5 % int2))) -> (rule8 % int1))
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is big.
("Charlie" "is" "big" "+")
int3
Dave is furry.
("Dave" "is" "furry" "+")
((triple2 ((((triple2) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is red.
("Dave" "is" "red" "+")
int2
Dave is big.
("Dave" "is" "big" "+")
int3
Charlie is furry.
("Charlie" "is" "furry" "+")
((((((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule8 % int2)) ((((triple1) -> (rule1 % int4))) -> (rule5 % int3))) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Charlie is quiet.
("Charlie" "is" "quiet" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
int3
Charlie is big.
("Charlie" "is" "big" "+")
int4