Anne is cold. Anne is nice. Anne is quiet. Bob is blue. Bob is kind. Bob is nice. Bob is red. Bob is young. Charlie is blue. Fiona is red. All blue things are red. If something is cold and quiet then it is kind. All blue things are kind. Red things are young. If Fiona is red then Fiona is blue. All cold things are blue.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is nice.
("Anne" "is" "nice" "+")
Anne is quiet.
("Anne" "is" "quiet" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
All blue things are red.
((("something" "is" "blue" "+")) -> ("something" "is" "red" "+"))
If something is cold and quiet then it is kind.
((("something" "is" "cold" "+") ("something" "is" "quiet" "+")) -> ("something" "is" "kind" "+"))
All blue things are kind.
((("something" "is" "blue" "+")) -> ("something" "is" "kind" "+"))
Red things are young.
((("something" "is" "red" "+")) -> ("something" "is" "young" "+"))
If Fiona is red then Fiona is blue.
((("Fiona" "is" "red" "+")) -> ("Fiona" "is" "blue" "+"))
All cold things are blue.
((("something" "is" "cold" "+")) -> ("something" "is" "blue" "+"))
Anne is quiet.
True
1
proof
[(triple3)]
("Anne" "is" "quiet" "+")
triple3
Bob is not kind.
False
1
inv-proof
[(triple5 OR ((triple4) -> rule3))]
("Bob" "is" "kind" "-")
triple5
((triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is not quiet.
Unknown
inv-random
[@0: Bob is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "quiet" "-")
Charlie is quiet.
Unknown
random
[@0: Charlie is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "quiet" "+")
@0: Anne is cold.[(triple1)] Anne is nice.[(triple2)] Anne is quiet.[(triple3)] Bob is blue.[(triple4)] Bob is kind.[(triple5 OR ((triple4) -> rule3))] Bob is nice.[(triple6)] Bob is red.[(triple7 OR ((triple4) -> rule1))] Bob is young.[(triple8 OR ((triple7) -> rule4) OR ((((triple4) -> rule1)) -> rule4))] Charlie is blue.[(triple9)] Fiona is red.[(triple10)] @1: Anne is blue.[(((triple1) -> rule6))] Anne is kind.[(((triple1 triple3) -> rule2) OR ((((triple1) -> rule6)) -> rule3))] Charlie is kind.[(((triple9) -> rule3))] Charlie is red.[(((triple9) -> rule1))] Fiona is blue.[(((triple10) -> rule5))] Fiona is young.[(((triple10) -> rule4))] @2: Anne is red.[(((((triple1) -> rule6)) -> rule1))] Charlie is young.[(((((triple9) -> rule1)) -> rule4))] Fiona is kind.[(((((triple10) -> rule5)) -> rule3))] @3: Anne is young.[(((((((triple1) -> rule6)) -> rule1)) -> rule4))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
Anne is nice.
("Anne" "is" "nice" "+")
triple2
Anne is quiet.
("Anne" "is" "quiet" "+")
triple3
Bob is blue.
("Bob" "is" "blue" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
((triple4) -> (rule3 % int1))
Bob is kind.
("Bob" "is" "kind" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
triple6
Bob is red.
("Bob" "is" "red" "+")
triple7
((triple4) -> (rule1 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple8
((triple7) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
((((triple4) -> (rule1 % int2))) -> (rule4 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Charlie is blue.
("Charlie" "is" "blue" "+")
triple9
Fiona is red.
("Fiona" "is" "red" "+")
triple10
Anne is blue.
("Anne" "is" "blue" "+")
((triple1) -> (rule6 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is kind.
("Anne" "is" "kind" "+")
((triple1 triple3) -> (rule2 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
((((triple1) -> (rule6 % int2))) -> (rule3 % int1))
Anne is kind.
("Anne" "is" "kind" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is kind.
("Charlie" "is" "kind" "+")
((triple9) -> (rule3 % int1))
Charlie is kind.
("Charlie" "is" "kind" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
((triple9) -> (rule1 % int1))
Charlie is red.
("Charlie" "is" "red" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
((triple10) -> (rule5 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
((triple10) -> (rule4 % int1))
Fiona is young.
("Fiona" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
((((triple1) -> (rule6 % int2))) -> (rule1 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Charlie is young.
("Charlie" "is" "young" "+")
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Charlie is young.
("Charlie" "is" "young" "+")
int1
Charlie is red.
("Charlie" "is" "red" "+")
int2
Fiona is kind.
("Fiona" "is" "kind" "+")
((((triple10) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
((((((triple1) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule4 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is blue.
("Anne" "is" "blue" "+")
int3