Harry is big. All green things are round. If something is big then it is round. White things are green. Red things are white. All round things are red. If something is green and not cold then it is smart. If something is red and not green then it is smart. If something is big and not round then it is smart.
Harry is big.
("Harry" "is" "big" "+")
All green things are round.
((("something" "is" "green" "+")) -> ("something" "is" "round" "+"))
If something is big then it is round.
((("something" "is" "big" "+")) -> ("something" "is" "round" "+"))
White things are green.
((("something" "is" "white" "+")) -> ("something" "is" "green" "+"))
Red things are white.
((("something" "is" "red" "+")) -> ("something" "is" "white" "+"))
All round things are red.
((("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
If something is green and not cold then it is smart.
((("something" "is" "green" "+") ("something" "is" "cold" "~")) -> ("something" "is" "smart" "+"))
If something is red and not green then it is smart.
((("something" "is" "red" "+") ("something" "is" "green" "~")) -> ("something" "is" "smart" "+"))
If something is big and not round then it is smart.
((("something" "is" "big" "+") ("something" "is" "round" "~")) -> ("something" "is" "smart" "+"))
Harry is big.
True
1
proof
[(triple1)]
("Harry" "is" "big" "+")
triple1
Harry is not big.
False
1
inv-proof
[(triple1)]
("Harry" "is" "big" "-")
triple1
Harry is round.
True
2
proof
[(((triple1) -> rule2))]
("Harry" "is" "round" "+")
((triple1) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is not round.
False
2
inv-proof
[(((triple1) -> rule2))]
("Harry" "is" "round" "-")
((triple1) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
True
3
proof
[(((((triple1) -> rule2)) -> rule5))]
("Harry" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is not red.
False
3
inv-proof
[(((((triple1) -> rule2)) -> rule5))]
("Harry" "is" "red" "-")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
True
4
proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule4))]
("Harry" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not white.
False
4
inv-proof
[(((((((triple1) -> rule2)) -> rule5)) -> rule4))]
("Harry" "is" "white" "-")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is not smart.
Unknown
inv-rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "smart" "-")
Harry is cold.
Unknown
random
[@0: Harry is cold.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "cold" "+")
@0: Harry is big.[(triple1)] @1: Harry is round.[(((triple1) -> rule2))] @2: Harry is red.[(((((triple1) -> rule2)) -> rule5))] @3: Harry is white.[(((((((triple1) -> rule2)) -> rule5)) -> rule4))] @4: Harry is green.[(((((((((triple1) -> rule2)) -> rule5)) -> rule4)) -> rule3))]
Harry is big.
("Harry" "is" "big" "+")
triple1
Harry is round.
("Harry" "is" "round" "+")
((triple1) -> (rule2 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple1) -> (rule2 % int2))) -> (rule5 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is round.
("Harry" "is" "round" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((((triple1) -> (rule2 % int3))) -> (rule5 % int2))) -> (rule4 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is round.
("Harry" "is" "round" "+")
int3
Harry is green.
("Harry" "is" "green" "+")
((((((((triple1) -> (rule2 % int4))) -> (rule5 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is red.
("Harry" "is" "red" "+")
int3
Harry is round.
("Harry" "is" "round" "+")
int4