Bob is round. Charlie is red. Harry is white. White, rough people are green. If Harry is white then Harry is red. All round, big people are white. Red people are furry. All red people are big. Red, big people are green.
Bob is round.
("Bob" "is" "round" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Harry is white.
("Harry" "is" "white" "+")
White, rough people are green.
((("someone" "is" "white" "+") ("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If Harry is white then Harry is red.
((("Harry" "is" "white" "+")) -> ("Harry" "is" "red" "+"))
All round, big people are white.
((("someone" "is" "round" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
Red people are furry.
((("someone" "is" "red" "+")) -> ("someone" "is" "furry" "+"))
All red people are big.
((("someone" "is" "red" "+")) -> ("someone" "is" "big" "+"))
Red, big people are green.
((("someone" "is" "red" "+") ("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Charlie is red.
True
1
proof
[(triple2)]
("Charlie" "is" "red" "+")
triple2
Harry is not white.
False
1
inv-proof
[(triple3)]
("Harry" "is" "white" "-")
triple3
Charlie is big.
True
2
proof
[(((triple2) -> rule5))]
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Harry is not red.
False
2
inv-proof
[(((triple3) -> rule2))]
("Harry" "is" "red" "-")
((triple3) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is furry.
True
3
proof
[(((((triple3) -> rule2)) -> rule4))]
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is not furry.
False
3
inv-proof
[(((((triple3) -> rule2)) -> rule4))]
("Harry" "is" "furry" "-")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
True
6
proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule6))]
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is not green.
False
6
inv-proof
[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule6))]
("Harry" "is" "green" "-")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Bob is not big.
Unknown
inv-rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Bob" "is" "big" "-")
Bob is furry.
Unknown
rconc
[@1: Bob is furry.[CWA. Example of deepest failure = (rule4 <- FAIL)]]
("Bob" "is" "furry" "+")
Bob is not white.
Unknown
inv-rconc
[@2: Bob is white.[CWA. Example of deepest failure = (rule3 <- rule5 <- FAIL)]]
("Bob" "is" "white" "-")
Bob is green.
Unknown
rconc
[@1: Bob is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "green" "+")
Charlie is not rough.
Unknown
inv-random
[@0: Charlie is rough.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "rough" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Harry is not round.
Unknown
inv-random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "-")
Bob is rough.
Unknown
random
[@0: Bob is rough.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "rough" "+")
@0: Bob is round.[(triple1)] Charlie is red.[(triple2)] Harry is white.[(triple3)] @1: Charlie is big.[(((triple2) -> rule5))] Charlie is furry.[(((triple2) -> rule4))] Harry is red.[(((triple3) -> rule2))] @2: Charlie is green.[(((triple2 ((triple2) -> rule5)) -> rule6))] Harry is big.[(((((triple3) -> rule2)) -> rule5))] Harry is furry.[(((((triple3) -> rule2)) -> rule4))] @3: Harry is green.[(((((triple3) -> rule2) ((((triple3) -> rule2)) -> rule5)) -> rule6))]
Bob is round.
("Bob" "is" "round" "+")
triple1
Charlie is red.
("Charlie" "is" "red" "+")
triple2
Harry is white.
("Harry" "is" "white" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
((triple2) -> (rule5 % int1))
Charlie is big.
("Charlie" "is" "big" "+")
int1
Charlie is furry.
("Charlie" "is" "furry" "+")
((triple2) -> (rule4 % int1))
Charlie is furry.
("Charlie" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple3) -> (rule2 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
((triple2 ((triple2) -> (rule5 % int2))) -> (rule6 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is big.
("Charlie" "is" "big" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
((((triple3) -> (rule2 % int2))) -> (rule5 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is furry.
("Harry" "is" "furry" "+")
((((triple3) -> (rule2 % int2))) -> (rule4 % int1))
Harry is furry.
("Harry" "is" "furry" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple3) -> (rule2 % int3)) ((((triple3) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3