Harry is big. Harry is blue. Harry is quiet. If someone is round then they are big. All round people are cold. All big, green people are white. Green, cold people are big. Quiet people are green. Big people are green.
Harry is big.
("Harry" "is" "big" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
If someone is round then they are big.
((("someone" "is" "round" "+")) -> ("someone" "is" "big" "+"))
All round people are cold.
((("someone" "is" "round" "+")) -> ("someone" "is" "cold" "+"))
All big, green people are white.
((("someone" "is" "big" "+") ("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Green, cold people are big.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "big" "+"))
Quiet people are green.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "green" "+"))
Big people are green.
((("someone" "is" "big" "+")) -> ("someone" "is" "green" "+"))
Harry is blue.
True
1
proof
[(triple2)]
("Harry" "is" "blue" "+")
triple2
Harry is not big.
False
1
inv-proof
[(triple1)]
("Harry" "is" "big" "-")
triple1
Harry is green.
True
2
proof
[(((triple1) -> rule6) OR ((triple3) -> rule5))]
("Harry" "is" "green" "+")
((triple1) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple3) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is not green.
False
2
inv-proof
[(((triple1) -> rule6) OR ((triple3) -> rule5))]
("Harry" "is" "green" "-")
((triple1) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple3) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
True
4
proof
[(((triple1 ((triple1) -> rule6)) -> rule3) OR ((triple1 ((triple3) -> rule5)) -> rule3))]
("Harry" "is" "white" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple1 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not white.
False
4
inv-proof
[(((triple1 ((triple1) -> rule6)) -> rule3) OR ((triple1 ((triple3) -> rule5)) -> rule3))]
("Harry" "is" "white" "-")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple1 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Harry" "is" "cold" "-")
Harry is round.
Unknown
random
[@0: Harry is round.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "round" "+")
@0: Harry is big.[(triple1)] Harry is blue.[(triple2)] Harry is quiet.[(triple3)] @1: Harry is green.[(((triple1) -> rule6) OR ((triple3) -> rule5))] @2: Harry is white.[(((triple1 ((triple1) -> rule6)) -> rule3) OR ((triple1 ((triple3) -> rule5)) -> rule3))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is blue.
("Harry" "is" "blue" "+")
triple2
Harry is quiet.
("Harry" "is" "quiet" "+")
triple3
Harry is green.
("Harry" "is" "green" "+")
((triple1) -> (rule6 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
((triple3) -> (rule5 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
((triple1 ((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
((triple1 ((triple3) -> (rule5 % int2))) -> (rule3 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2