Bob is big. Bob is cold. Bob is not nice. Bob is not red. Bob is not young. Charlie is big. Charlie is kind. Charlie is nice. Charlie is round. Charlie is young. Dave is young. Erin is not big. All nice, round things are red. Nice, red things are not cold. If something is kind and not young then it is not nice.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is not nice.
("Bob" "is" "nice" "-")
Bob is not red.
("Bob" "is" "red" "-")
Bob is not young.
("Bob" "is" "young" "-")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Charlie is young.
("Charlie" "is" "young" "+")
Dave is young.
("Dave" "is" "young" "+")
Erin is not big.
("Erin" "is" "big" "-")
All nice, round things are red.
((("something" "is" "nice" "+") ("something" "is" "round" "+")) -> ("something" "is" "red" "+"))
Nice, red things are not cold.
((("something" "is" "nice" "+") ("something" "is" "red" "+")) -> ("something" "is" "cold" "-"))
If something is kind and not young then it is not nice.
((("something" "is" "kind" "+") ("something" "is" "young" "~")) -> ("something" "is" "nice" "-"))
Bob is not red.
True
1
proof
[(triple4)]
("Bob" "is" "red" "-")
triple4
Charlie is not big.
False
1
inv-proof
[(triple6)]
("Charlie" "is" "big" "-")
triple6
Charlie is red.
True
3
proof
[(((triple8 triple9) -> rule1))]
("Charlie" "is" "red" "+")
((triple8 triple9) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not red.
False
3
inv-proof
[(((triple8 triple9) -> rule1))]
("Charlie" "is" "red" "-")
((triple8 triple9) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not cold.
True
5
proof
[(((triple8 ((triple8 triple9) -> rule1)) -> rule2))]
("Charlie" "is" "cold" "-")
((triple8 ((triple8 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Charlie is cold.
False
5
inv-proof
[(((triple8 ((triple8 triple9) -> rule1)) -> rule2))]
("Charlie" "is" "cold" "+")
((triple8 ((triple8 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Dave is not red.
Unknown
inv-rconc
[@1: Dave is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "red" "-")
Erin is red.
Unknown
rconc
[@1: Erin is red.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Erin" "is" "red" "+")
Dave is not big.
Unknown
inv-random
[@0: Dave is big.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "big" "-")
Dave is nice.
Unknown
random
[@0: Dave is nice.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "nice" "+")
Erin is not cold.
Unknown
inv-random
[@0: Erin is cold.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "cold" "-")
Erin is kind.
Unknown
random
[@0: Erin is kind.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "kind" "+")
@0: Bob is big.[(triple1)] Bob is cold.[(triple2)] Bob is not nice.[(triple3)] Bob is not red.[(triple4)] Bob is not young.[(triple5)] Charlie is big.[(triple6)] Charlie is kind.[(triple7)] Charlie is nice.[(triple8)] Charlie is round.[(triple9)] Charlie is young.[(triple10)] Dave is young.[(triple11)] Erin is not big.[(triple12)] @1: Charlie is red.[(((triple8 triple9) -> rule1))] @2: Charlie is not cold.[(((triple8 ((triple8 triple9) -> rule1)) -> rule2))]
Bob is big.
("Bob" "is" "big" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is not nice.
("Bob" "is" "nice" "-")
triple3
Bob is not red.
("Bob" "is" "red" "-")
triple4
Bob is not young.
("Bob" "is" "young" "-")
triple5
Charlie is big.
("Charlie" "is" "big" "+")
triple6
Charlie is kind.
("Charlie" "is" "kind" "+")
triple7
Charlie is nice.
("Charlie" "is" "nice" "+")
triple8
Charlie is round.
("Charlie" "is" "round" "+")
triple9
Charlie is young.
("Charlie" "is" "young" "+")
triple10
Dave is young.
("Dave" "is" "young" "+")
triple11
Erin is not big.
("Erin" "is" "big" "-")
triple12
Charlie is red.
("Charlie" "is" "red" "+")
((triple8 triple9) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Charlie is not cold.
("Charlie" "is" "cold" "-")
((triple8 ((triple8 triple9) -> (rule1 % int2))) -> (rule2 % int1))
Charlie is not cold.
("Charlie" "is" "cold" "-")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2