Anne is cold. Anne is young. Bob is blue. Bob is cold. Bob is kind. Bob is red. Bob is young. Fiona is blue. Fiona is red. Fiona is smart. Red, young people are smart. If Anne is smart then Anne is cold. All blue people are smart. Rough, red people are smart. If Fiona is rough and Fiona is blue then Fiona is red. If someone is young then they are smart. Red people are blue. If someone is cold then they are red.
Anne is cold.
("Anne" "is" "cold" "+")
Anne is young.
("Anne" "is" "young" "+")
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Red, young people are smart.
((("someone" "is" "red" "+") ("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
If Anne is smart then Anne is cold.
((("Anne" "is" "smart" "+")) -> ("Anne" "is" "cold" "+"))
All blue people are smart.
((("someone" "is" "blue" "+")) -> ("someone" "is" "smart" "+"))
Rough, red people are smart.
((("someone" "is" "rough" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "smart" "+"))
If Fiona is rough and Fiona is blue then Fiona is red.
((("Fiona" "is" "rough" "+") ("Fiona" "is" "blue" "+")) -> ("Fiona" "is" "red" "+"))
If someone is young then they are smart.
((("someone" "is" "young" "+")) -> ("someone" "is" "smart" "+"))
Red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If someone is cold then they are red.
((("someone" "is" "cold" "+")) -> ("someone" "is" "red" "+"))
Fiona is smart.
True
1
proof
[(triple10 OR ((triple8) -> rule3) OR ((((triple9) -> rule7)) -> rule3))]
("Fiona" "is" "smart" "+")
triple10
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Fiona is not smart.
False
1
inv-proof
[(triple10 OR ((triple8) -> rule3) OR ((((triple9) -> rule7)) -> rule3))]
("Fiona" "is" "smart" "-")
triple10
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Anne is not kind.
Unknown
inv-random
[@0: Anne is kind.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "kind" "-")
Fiona is cold.
Unknown
random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "+")
@0: Anne is cold.[(triple1 OR ((((triple2) -> rule6)) -> rule2))] Anne is young.[(triple2)] Bob is blue.[(triple3 OR ((triple6) -> rule7) OR ((((triple4) -> rule8)) -> rule7))] Bob is cold.[(triple4)] Bob is kind.[(triple5)] Bob is red.[(triple6 OR ((triple4) -> rule8))] Bob is young.[(triple7)] Fiona is blue.[(triple8 OR ((triple9) -> rule7))] Fiona is red.[(triple9)] Fiona is smart.[(triple10 OR ((triple8) -> rule3) OR ((((triple9) -> rule7)) -> rule3))] @1: Anne is red.[(((triple1) -> rule8) OR ((((((triple2) -> rule6)) -> rule2)) -> rule8))] Anne is smart.[(((triple2) -> rule6) OR ((((triple1) -> rule8) triple2) -> rule1) OR ((((((triple1) -> rule8)) -> rule7)) -> rule3))] Bob is smart.[(((triple3) -> rule3) OR ((triple7) -> rule6) OR ((triple6 triple7) -> rule1) OR ((((triple6) -> rule7)) -> rule3) OR ((((triple4) -> rule8) triple7) -> rule1) OR ((((((triple4) -> rule8)) -> rule7)) -> rule3))] @2: Anne is blue.[(((((triple1) -> rule8)) -> rule7) OR ((((((((triple2) -> rule6)) -> rule2)) -> rule8)) -> rule7))]
Anne is cold.
("Anne" "is" "cold" "+")
triple1
((((triple2) -> (rule6 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is smart.
("Anne" "is" "smart" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
triple2
Bob is blue.
("Bob" "is" "blue" "+")
triple3
((triple6) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
((((triple4) -> (rule8 % int2))) -> (rule7 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple4
Bob is kind.
("Bob" "is" "kind" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
((triple4) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple7
Fiona is blue.
("Fiona" "is" "blue" "+")
triple8
((triple9) -> (rule7 % int1))
Fiona is blue.
("Fiona" "is" "blue" "+")
int1
Fiona is red.
("Fiona" "is" "red" "+")
triple9
Fiona is smart.
("Fiona" "is" "smart" "+")
triple10
((triple8) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
((((triple9) -> (rule7 % int2))) -> (rule3 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
((triple1) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
((((((triple2) -> (rule6 % int3))) -> (rule2 % int2))) -> (rule8 % int1))
Anne is red.
("Anne" "is" "red" "+")
int1
Anne is cold.
("Anne" "is" "cold" "+")
int2
Anne is smart.
("Anne" "is" "smart" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
((triple2) -> (rule6 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
((((triple1) -> (rule8 % int2)) triple2) -> (rule1 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((triple1) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Anne is smart.
("Anne" "is" "smart" "+")
int1
Anne is blue.
("Anne" "is" "blue" "+")
int2
Anne is red.
("Anne" "is" "red" "+")
int3
Bob is smart.
("Bob" "is" "smart" "+")
((triple3) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple7) -> (rule6 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((triple6 triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
((((triple6) -> (rule7 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
((((triple4) -> (rule8 % int2)) triple7) -> (rule1 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
int2
((((((triple4) -> (rule8 % int3))) -> (rule7 % int2))) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Bob is red.
("Bob" "is" "red" "+")
int3
Anne is blue.
("Anne" "is" "blue" "+")
((((triple1) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
((((((((triple2) -> (rule6 % int4))) -> (rule2 % int3))) -> (rule8 % int2))) -> (rule7 % int1))
Anne is blue.
("Anne" "is" "blue" "+")
int1
Anne is red.
("Anne" "is" "red" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
int3
Anne is smart.
("Anne" "is" "smart" "+")
int4