Bob is green. Erin is big. Erin is cold. Erin is rough. Erin is round. Erin is smart. Fiona is blue. Fiona is round. Harry is blue. Harry is smart. If something is blue then it is big. Smart things are cold. If Fiona is smart then Fiona is cold. Big things are smart. Big, rough things are green. If Bob is green then Bob is cold.
Bob is green.
("Bob" "is" "green" "+")
Erin is big.
("Erin" "is" "big" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Erin is smart.
("Erin" "is" "smart" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is smart.
("Harry" "is" "smart" "+")
If something is blue then it is big.
((("something" "is" "blue" "+")) -> ("something" "is" "big" "+"))
Smart things are cold.
((("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
If Fiona is smart then Fiona is cold.
((("Fiona" "is" "smart" "+")) -> ("Fiona" "is" "cold" "+"))
Big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
Big, rough things are green.
((("something" "is" "big" "+") ("something" "is" "rough" "+")) -> ("something" "is" "green" "+"))
If Bob is green then Bob is cold.
((("Bob" "is" "green" "+")) -> ("Bob" "is" "cold" "+"))
Erin is round.
True
1
proof
[(triple5)]
("Erin" "is" "round" "+")
triple5
Fiona is not blue.
False
1
inv-proof
[(triple7)]
("Fiona" "is" "blue" "-")
triple7
Fiona is big.
True
2
proof
[(((triple7) -> rule1))]
("Fiona" "is" "big" "+")
((triple7) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is not cold.
False
2
inv-proof
[(((triple1) -> rule6))]
("Bob" "is" "cold" "-")
((triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Fiona is smart.
True
3
proof
[(((((triple7) -> rule1)) -> rule4))]
("Fiona" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is not smart.
False
3
inv-proof
[(((((triple7) -> rule1)) -> rule4))]
("Fiona" "is" "smart" "-")
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
True
4
proof
[(((((((triple7) -> rule1)) -> rule4)) -> rule2) OR ((((((triple7) -> rule1)) -> rule4)) -> rule3))]
("Fiona" "is" "cold" "+")
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Fiona is not cold.
False
4
inv-proof
[(((((((triple7) -> rule1)) -> rule4)) -> rule2) OR ((((((triple7) -> rule1)) -> rule4)) -> rule3))]
("Fiona" "is" "cold" "-")
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
Bob is not smart.
Unknown
inv-rconc
[@2: Bob is smart.[CWA. Example of deepest failure = (rule4 <- rule1 <- FAIL)]]
("Bob" "is" "smart" "-")
Bob is big.
Unknown
rconc
[@1: Bob is big.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Bob" "is" "big" "+")
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Fiona" "is" "green" "-")
Harry is green.
Unknown
rconc
[@1: Harry is green.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Harry" "is" "green" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Bob is round.
Unknown
random
[@0: Bob is round.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "round" "+")
Bob is not blue.
Unknown
inv-random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "-")
Erin is blue.
Unknown
random
[@0: Erin is blue.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "blue" "+")
@0: Bob is green.[(triple1)] Erin is big.[(triple2)] Erin is cold.[(triple3 OR ((triple6) -> rule2) OR ((((triple2) -> rule4)) -> rule2))] Erin is rough.[(triple4)] Erin is round.[(triple5)] Erin is smart.[(triple6 OR ((triple2) -> rule4))] Fiona is blue.[(triple7)] Fiona is round.[(triple8)] Harry is blue.[(triple9)] Harry is smart.[(triple10 OR ((((triple9) -> rule1)) -> rule4))] @1: Bob is cold.[(((triple1) -> rule6))] Erin is green.[(((triple2 triple4) -> rule5))] Fiona is big.[(((triple7) -> rule1))] Harry is big.[(((triple9) -> rule1))] Harry is cold.[(((triple10) -> rule2) OR ((((((triple9) -> rule1)) -> rule4)) -> rule2))] @2: Fiona is smart.[(((((triple7) -> rule1)) -> rule4))] @3: Fiona is cold.[(((((((triple7) -> rule1)) -> rule4)) -> rule2) OR ((((((triple7) -> rule1)) -> rule4)) -> rule3))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Erin is big.
("Erin" "is" "big" "+")
triple2
Erin is cold.
("Erin" "is" "cold" "+")
triple3
((triple6) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
((((triple2) -> (rule4 % int2))) -> (rule2 % int1))
Erin is cold.
("Erin" "is" "cold" "+")
int1
Erin is smart.
("Erin" "is" "smart" "+")
int2
Erin is rough.
("Erin" "is" "rough" "+")
triple4
Erin is round.
("Erin" "is" "round" "+")
triple5
Erin is smart.
("Erin" "is" "smart" "+")
triple6
((triple2) -> (rule4 % int1))
Erin is smart.
("Erin" "is" "smart" "+")
int1
Fiona is blue.
("Fiona" "is" "blue" "+")
triple7
Fiona is round.
("Fiona" "is" "round" "+")
triple8
Harry is blue.
("Harry" "is" "blue" "+")
triple9
Harry is smart.
("Harry" "is" "smart" "+")
triple10
((((triple9) -> (rule1 % int2))) -> (rule4 % int1))
Harry is smart.
("Harry" "is" "smart" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
((triple2 triple4) -> (rule5 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
((triple7) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple9) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((((triple9) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is smart.
("Harry" "is" "smart" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Fiona is smart.
("Fiona" "is" "smart" "+")
((((triple7) -> (rule1 % int2))) -> (rule4 % int1))
Fiona is smart.
("Fiona" "is" "smart" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3
((((((triple7) -> (rule1 % int3))) -> (rule4 % int2))) -> (rule3 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Fiona is smart.
("Fiona" "is" "smart" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
int3