Bob is blue. Bob is cold. Bob is green. Bob is kind. Bob is nice. Bob is rough. Bob is round. Charlie is blue. Charlie is green. Charlie is kind. Charlie is nice. Charlie is round. Fiona is blue. Fiona is green. Fiona is nice. Fiona is round. All green people are rough. Green, cold people are kind. If someone is kind then they are green. All rough people are kind. Kind, cold people are nice. If someone is nice and round then they are rough.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is round.
("Bob" "is" "round" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is green.
("Charlie" "is" "green" "+")
Charlie is kind.
("Charlie" "is" "kind" "+")
Charlie is nice.
("Charlie" "is" "nice" "+")
Charlie is round.
("Charlie" "is" "round" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is green.
("Fiona" "is" "green" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is round.
("Fiona" "is" "round" "+")
All green people are rough.
((("someone" "is" "green" "+")) -> ("someone" "is" "rough" "+"))
Green, cold people are kind.
((("someone" "is" "green" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "kind" "+"))
If someone is kind then they are green.
((("someone" "is" "kind" "+")) -> ("someone" "is" "green" "+"))
All rough people are kind.
((("someone" "is" "rough" "+")) -> ("someone" "is" "kind" "+"))
Kind, cold people are nice.
((("someone" "is" "kind" "+") ("someone" "is" "cold" "+")) -> ("someone" "is" "nice" "+"))
If someone is nice and round then they are rough.
((("someone" "is" "nice" "+") ("someone" "is" "round" "+")) -> ("someone" "is" "rough" "+"))
Bob is kind.
True
1
proof
[(triple4 OR ((triple6) -> rule4) OR ((triple3 triple2) -> rule2) OR ((((triple3) -> rule1)) -> rule4) OR ((((triple5 triple7) -> rule6)) -> rule4))]
("Bob" "is" "kind" "+")
triple4
((triple6) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Charlie is not nice.
False
1
inv-proof
[(triple11)]
("Charlie" "is" "nice" "-")
triple11
Charlie is rough.
True
2
proof
[(((triple9) -> rule1) OR ((triple11 triple12) -> rule6) OR ((((triple10) -> rule3)) -> rule1))]
("Charlie" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple11 triple12) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Charlie is not rough.
False
2
inv-proof
[(((triple9) -> rule1) OR ((triple11 triple12) -> rule6) OR ((((triple10) -> rule3)) -> rule1))]
("Charlie" "is" "rough" "-")
((triple9) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple11 triple12) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is kind.
True
3
proof
[(((((triple14) -> rule1)) -> rule4) OR ((((triple15 triple16) -> rule6)) -> rule4))]
("Fiona" "is" "kind" "+")
((((triple14) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple15 triple16) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not kind.
False
3
inv-proof
[(((((triple14) -> rule1)) -> rule4) OR ((((triple15 triple16) -> rule6)) -> rule4))]
("Fiona" "is" "kind" "-")
((((triple14) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple15 triple16) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Charlie is cold.
Unknown
random
[@0: Charlie is cold.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "cold" "+")
@0: Bob is blue.[(triple1)] Bob is cold.[(triple2)] Bob is green.[(triple3 OR ((triple4) -> rule3) OR ((((triple6) -> rule4)) -> rule3) OR ((((((triple5 triple7) -> rule6)) -> rule4)) -> rule3))] Bob is kind.[(triple4 OR ((triple6) -> rule4) OR ((triple3 triple2) -> rule2) OR ((((triple3) -> rule1)) -> rule4) OR ((((triple5 triple7) -> rule6)) -> rule4))] Bob is nice.[(triple5 OR ((triple4 triple2) -> rule5) OR ((((triple6) -> rule4) triple2) -> rule5) OR ((((triple3 triple2) -> rule2) triple2) -> rule5) OR ((((((triple3) -> rule1)) -> rule4) triple2) -> rule5))] Bob is rough.[(triple6 OR ((triple3) -> rule1) OR ((triple5 triple7) -> rule6) OR ((((triple4) -> rule3)) -> rule1) OR ((((triple4 triple2) -> rule5) triple7) -> rule6) OR ((((((triple3 triple2) -> rule2) triple2) -> rule5) triple7) -> rule6))] Bob is round.[(triple7)] Charlie is blue.[(triple8)] Charlie is green.[(triple9 OR ((triple10) -> rule3) OR ((((((triple11 triple12) -> rule6)) -> rule4)) -> rule3))] Charlie is kind.[(triple10 OR ((((triple9) -> rule1)) -> rule4) OR ((((triple11 triple12) -> rule6)) -> rule4))] Charlie is nice.[(triple11)] Charlie is round.[(triple12)] Fiona is blue.[(triple13)] Fiona is green.[(triple14 OR ((((((triple15 triple16) -> rule6)) -> rule4)) -> rule3))] Fiona is nice.[(triple15)] Fiona is round.[(triple16)] @1: Charlie is rough.[(((triple9) -> rule1) OR ((triple11 triple12) -> rule6) OR ((((triple10) -> rule3)) -> rule1))] Fiona is rough.[(((triple14) -> rule1) OR ((triple15 triple16) -> rule6))] @2: Fiona is kind.[(((((triple14) -> rule1)) -> rule4) OR ((((triple15 triple16) -> rule6)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple4) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((((triple6) -> (rule4 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple5 triple7) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is kind.
("Bob" "is" "kind" "+")
triple4
((triple6) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((triple3 triple2) -> (rule2 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
((((triple3) -> (rule1 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
((((triple5 triple7) -> (rule6 % int2))) -> (rule4 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
triple5
((triple4 triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
((((triple6) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((triple3 triple2) -> (rule2 % int2)) triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
((((((triple3) -> (rule1 % int3))) -> (rule4 % int2)) triple2) -> (rule5 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Bob is kind.
("Bob" "is" "kind" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
int3
Bob is rough.
("Bob" "is" "rough" "+")
triple6
((triple3) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple5 triple7) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule1 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple4 triple2) -> (rule5 % int2)) triple7) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
((((((triple3 triple2) -> (rule2 % int3)) triple2) -> (rule5 % int2)) triple7) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is kind.
("Bob" "is" "kind" "+")
int3
Bob is round.
("Bob" "is" "round" "+")
triple7
Charlie is blue.
("Charlie" "is" "blue" "+")
triple8
Charlie is green.
("Charlie" "is" "green" "+")
triple9
((triple10) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
((((((triple11 triple12) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Charlie is green.
("Charlie" "is" "green" "+")
int1
Charlie is kind.
("Charlie" "is" "kind" "+")
int2
Charlie is rough.
("Charlie" "is" "rough" "+")
int3
Charlie is kind.
("Charlie" "is" "kind" "+")
triple10
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
((((triple11 triple12) -> (rule6 % int2))) -> (rule4 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is rough.
("Charlie" "is" "rough" "+")
int2
Charlie is nice.
("Charlie" "is" "nice" "+")
triple11
Charlie is round.
("Charlie" "is" "round" "+")
triple12
Fiona is blue.
("Fiona" "is" "blue" "+")
triple13
Fiona is green.
("Fiona" "is" "green" "+")
triple14
((((((triple15 triple16) -> (rule6 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is nice.
("Fiona" "is" "nice" "+")
triple15
Fiona is round.
("Fiona" "is" "round" "+")
triple16
Charlie is rough.
("Charlie" "is" "rough" "+")
((triple9) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple11 triple12) -> (rule6 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple10) -> (rule3 % int2))) -> (rule1 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is green.
("Charlie" "is" "green" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple14) -> (rule1 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((triple15 triple16) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple14) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
((((triple15 triple16) -> (rule6 % int2))) -> (rule4 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2