Charlie is round. Dave is round. Harry is rough. Round people are nice. If Charlie is round and Charlie is red then Charlie is cold. If someone is nice then they are red. All rough, nice people are blue. If Charlie is rough and Charlie is red then Charlie is furry. Nice people are blue.
Charlie is round.
("Charlie" "is" "round" "+")
Dave is round.
("Dave" "is" "round" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Round people are nice.
((("someone" "is" "round" "+")) -> ("someone" "is" "nice" "+"))
If Charlie is round and Charlie is red then Charlie is cold.
((("Charlie" "is" "round" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "cold" "+"))
If someone is nice then they are red.
((("someone" "is" "nice" "+")) -> ("someone" "is" "red" "+"))
All rough, nice people are blue.
((("someone" "is" "rough" "+") ("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is rough and Charlie is red then Charlie is furry.
((("Charlie" "is" "rough" "+") ("Charlie" "is" "red" "+")) -> ("Charlie" "is" "furry" "+"))
Nice people are blue.
((("someone" "is" "nice" "+")) -> ("someone" "is" "blue" "+"))
Dave is round.
True
1
proof
[(triple2)]
("Dave" "is" "round" "+")
triple2
Dave is not round.
False
1
inv-proof
[(triple2)]
("Dave" "is" "round" "-")
triple2
Charlie is nice.
True
2
proof
[(((triple1) -> rule1))]
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is not nice.
False
2
inv-proof
[(((triple2) -> rule1))]
("Dave" "is" "nice" "-")
((triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Dave is red.
True
3
proof
[(((((triple2) -> rule1)) -> rule3))]
("Dave" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Charlie is not blue.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule6))]
("Charlie" "is" "blue" "-")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is cold.
True
5
proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not cold.
False
5
inv-proof
[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))]
("Charlie" "is" "cold" "-")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3
Charlie is not furry.
Unknown
inv-rconc
[@1: Charlie is furry.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Charlie" "is" "furry" "-")
Harry is red.
Unknown
rconc
[@2: Harry is red.[CWA. Example of deepest failure = (rule3 <- rule1 <- FAIL)]]
("Harry" "is" "red" "+")
Harry is not nice.
Unknown
inv-rconc
[@1: Harry is nice.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Harry" "is" "nice" "-")
Harry is blue.
Unknown
rconc
[@2: Harry is blue.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Harry" "is" "blue" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Dave is furry.
Unknown
random
[@0: Dave is furry.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "furry" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Dave is cold.
Unknown
random
[@0: Dave is cold.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "cold" "+")
@0: Charlie is round.[(triple1)] Dave is round.[(triple2)] Harry is rough.[(triple3)] @1: Charlie is nice.[(((triple1) -> rule1))] Dave is nice.[(((triple2) -> rule1))] @2: Charlie is blue.[(((((triple1) -> rule1)) -> rule6))] Charlie is red.[(((((triple1) -> rule1)) -> rule3))] Dave is blue.[(((((triple2) -> rule1)) -> rule6))] Dave is red.[(((((triple2) -> rule1)) -> rule3))] @3: Charlie is cold.[(((triple1 ((((triple1) -> rule1)) -> rule3)) -> rule2))]
Charlie is round.
("Charlie" "is" "round" "+")
triple1
Dave is round.
("Dave" "is" "round" "+")
triple2
Harry is rough.
("Harry" "is" "rough" "+")
triple3
Charlie is nice.
("Charlie" "is" "nice" "+")
((triple1) -> (rule1 % int1))
Charlie is nice.
("Charlie" "is" "nice" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
((triple2) -> (rule1 % int1))
Dave is nice.
("Dave" "is" "nice" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((((triple1) -> (rule1 % int2))) -> (rule6 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Charlie is red.
("Charlie" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule3 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is nice.
("Charlie" "is" "nice" "+")
int2
Dave is blue.
("Dave" "is" "blue" "+")
((((triple2) -> (rule1 % int2))) -> (rule6 % int1))
Dave is blue.
("Dave" "is" "blue" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Dave is red.
("Dave" "is" "red" "+")
((((triple2) -> (rule1 % int2))) -> (rule3 % int1))
Dave is red.
("Dave" "is" "red" "+")
int1
Dave is nice.
("Dave" "is" "nice" "+")
int2
Charlie is cold.
("Charlie" "is" "cold" "+")
((triple1 ((((triple1) -> (rule1 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Charlie is cold.
("Charlie" "is" "cold" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
int3