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