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