Bob is cold. Bob is kind. Harry is green. Harry is kind. Harry is round. Harry is white. Harry is young. Green things are white. If Bob is not kind then Bob is red. All kind things are green. If Harry is green then Harry is round. If something is round and not white then it is cold. If something is cold then it is young. All kind, white things are red. If something is green and not young then it is not red.
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
Green things are white.
((("something" "is" "green" "+")) -> ("something" "is" "white" "+"))
If Bob is not kind then Bob is red.
((("Bob" "is" "kind" "~")) -> ("Bob" "is" "red" "+"))
All kind things are green.
((("something" "is" "kind" "+")) -> ("something" "is" "green" "+"))
If Harry is green then Harry is round.
((("Harry" "is" "green" "+")) -> ("Harry" "is" "round" "+"))
If something is round and not white then it is cold.
((("something" "is" "round" "+") ("something" "is" "white" "~")) -> ("something" "is" "cold" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
All kind, white things are red.
((("something" "is" "kind" "+") ("something" "is" "white" "+")) -> ("something" "is" "red" "+"))
If something is green and not young then it is not red.
((("something" "is" "green" "+") ("something" "is" "young" "~")) -> ("something" "is" "red" "-"))
Harry is young.
True
1
proof
[(triple7)]
("Harry" "is" "young" "+")
triple7
Harry is not young.
False
1
inv-proof
[(triple7)]
("Harry" "is" "young" "-")
triple7
Harry is red.
True
3
proof
[(((triple4 triple6) -> rule7) OR ((triple4 ((triple3) -> rule1)) -> rule7) OR ((triple4 ((((triple4) -> rule3)) -> rule1)) -> rule7))]
("Harry" "is" "red" "+")
((triple4 triple6) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple4 ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is not green.
False
2
inv-proof
[(((triple2) -> rule3))]
("Bob" "is" "green" "-")
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
True
3
proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple2) -> rule3)) -> rule1))]
("Bob" "is" "white" "-")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
True
5
proof
[(((triple2 ((((triple2) -> rule3)) -> rule1)) -> rule7))]
("Bob" "is" "red" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is not red.
False
5
inv-proof
[(((triple2 ((((triple2) -> rule3)) -> rule1)) -> rule7))]
("Bob" "is" "red" "-")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Harry is not cold.
Unknown
inv-rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "cold" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
@0: Bob is cold.[(triple1)] Bob is kind.[(triple2)] Harry is green.[(triple3 OR ((triple4) -> rule3))] Harry is kind.[(triple4)] Harry is round.[(triple5 OR ((triple3) -> rule4) OR ((((triple4) -> rule3)) -> rule4))] Harry is white.[(triple6 OR ((triple3) -> rule1) OR ((((triple4) -> rule3)) -> rule1))] Harry is young.[(triple7)] @1: Bob is green.[(((triple2) -> rule3))] Bob is young.[(((triple1) -> rule6))] Harry is red.[(((triple4 triple6) -> rule7) OR ((triple4 ((triple3) -> rule1)) -> rule7) OR ((triple4 ((((triple4) -> rule3)) -> rule1)) -> rule7))] @2: Bob is white.[(((((triple2) -> rule3)) -> rule1))] @3: Bob is red.[(((triple2 ((((triple2) -> rule3)) -> rule1)) -> rule7))]
Bob is cold.
("Bob" "is" "cold" "+")
triple1
Bob is kind.
("Bob" "is" "kind" "+")
triple2
Harry is green.
("Harry" "is" "green" "+")
triple3
((triple4) -> (rule3 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
triple4
Harry is round.
("Harry" "is" "round" "+")
triple5
((triple3) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule4 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
triple6
((triple3) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
triple7
Bob is green.
("Bob" "is" "green" "+")
((triple2) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
((triple1) -> (rule6 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((triple4 triple6) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
((triple4 ((triple3) -> (rule1 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((triple4 ((((triple4) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule3 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
((triple2 ((((triple2) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule7 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3