Bob is blue. Bob is cold. Bob is kind. Charlie is big. Charlie is blue. Charlie is cold. Charlie is red. Charlie is rough. Fiona is big. Fiona is rough. Harry is cold. Harry is red. If Fiona is white then Fiona is blue. Kind people are rough. If someone is big then they are rough. All blue people are rough. All red people are blue. If Charlie is kind and Charlie is blue then Charlie is white. Kind, white people are red. Cold people are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is kind.
("Bob" "is" "kind" "+")
Charlie is big.
("Charlie" "is" "big" "+")
Charlie is blue.
("Charlie" "is" "blue" "+")
Charlie is cold.
("Charlie" "is" "cold" "+")
Charlie is red.
("Charlie" "is" "red" "+")
Charlie is rough.
("Charlie" "is" "rough" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is red.
("Harry" "is" "red" "+")
If Fiona is white then Fiona is blue.
((("Fiona" "is" "white" "+")) -> ("Fiona" "is" "blue" "+"))
Kind people are rough.
((("someone" "is" "kind" "+")) -> ("someone" "is" "rough" "+"))
If someone is big then they are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
All blue people are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
All red people are blue.
((("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
If Charlie is kind and Charlie is blue then Charlie is white.
((("Charlie" "is" "kind" "+") ("Charlie" "is" "blue" "+")) -> ("Charlie" "is" "white" "+"))
Kind, white people are red.
((("someone" "is" "kind" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Cold people are blue.
((("someone" "is" "cold" "+")) -> ("someone" "is" "blue" "+"))
Charlie is cold.
True
1
proof
[(triple6)]
("Charlie" "is" "cold" "+")
triple6
Fiona is not big.
False
1
inv-proof
[(triple9)]
("Fiona" "is" "big" "-")
triple9
Bob is rough.
True
2
proof
[(((triple1) -> rule4) OR ((triple3) -> rule2) OR ((((triple2) -> rule8)) -> rule4))]
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Harry is not blue.
False
2
inv-proof
[(((triple11) -> rule8) OR ((triple12) -> rule5))]
("Harry" "is" "blue" "-")
((triple11) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple12) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
True
3
proof
[(((((triple11) -> rule8)) -> rule4) OR ((((triple12) -> rule5)) -> rule4))]
("Harry" "is" "rough" "+")
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Harry is not rough.
False
3
inv-proof
[(((((triple11) -> rule8)) -> rule4) OR ((((triple12) -> rule5)) -> rule4))]
("Harry" "is" "rough" "-")
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
Bob is not red.
Unknown
inv-rconc
[@1: Bob is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Bob" "is" "red" "-")
Fiona is red.
Unknown
rconc
[@1: Fiona is red.[CWA. Example of deepest failure = (rule7 <- FAIL)]]
("Fiona" "is" "red" "+")
Fiona is not blue.
Unknown
inv-rconc
[@2: Fiona is blue.[CWA. Example of deepest failure = (rule5 <- rule7 <- FAIL)]]
("Fiona" "is" "blue" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
Bob is not big.
Unknown
inv-random
[@0: Bob is big.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "big" "-")
Fiona is kind.
Unknown
random
[@0: Fiona is kind.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "kind" "+")
@0: Bob is blue.[(triple1 OR ((triple2) -> rule8))] Bob is cold.[(triple2)] Bob is kind.[(triple3)] Charlie is big.[(triple4)] Charlie is blue.[(triple5 OR ((triple6) -> rule8) OR ((triple7) -> rule5))] Charlie is cold.[(triple6)] Charlie is red.[(triple7)] Charlie is rough.[(triple8 OR ((triple4) -> rule3) OR ((triple5) -> rule4) OR ((((triple6) -> rule8)) -> rule4) OR ((((triple7) -> rule5)) -> rule4))] Fiona is big.[(triple9)] Fiona is rough.[(triple10 OR ((triple9) -> rule3))] Harry is cold.[(triple11)] Harry is red.[(triple12)] @1: Bob is rough.[(((triple1) -> rule4) OR ((triple3) -> rule2) OR ((((triple2) -> rule8)) -> rule4))] Harry is blue.[(((triple11) -> rule8) OR ((triple12) -> rule5))] @2: Harry is rough.[(((((triple11) -> rule8)) -> rule4) OR ((((triple12) -> rule5)) -> rule4))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
((triple2) -> (rule8 % int1))
Bob is blue.
("Bob" "is" "blue" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
triple2
Bob is kind.
("Bob" "is" "kind" "+")
triple3
Charlie is big.
("Charlie" "is" "big" "+")
triple4
Charlie is blue.
("Charlie" "is" "blue" "+")
triple5
((triple6) -> (rule8 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
((triple7) -> (rule5 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Charlie is cold.
("Charlie" "is" "cold" "+")
triple6
Charlie is red.
("Charlie" "is" "red" "+")
triple7
Charlie is rough.
("Charlie" "is" "rough" "+")
triple8
((triple4) -> (rule3 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((triple5) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
((((triple6) -> (rule8 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
((((triple7) -> (rule5 % int2))) -> (rule4 % int1))
Charlie is rough.
("Charlie" "is" "rough" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
int2
Fiona is big.
("Fiona" "is" "big" "+")
triple9
Fiona is rough.
("Fiona" "is" "rough" "+")
triple10
((triple9) -> (rule3 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Harry is cold.
("Harry" "is" "cold" "+")
triple11
Harry is red.
("Harry" "is" "red" "+")
triple12
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((triple2) -> (rule8 % int2))) -> (rule4 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is blue.
("Bob" "is" "blue" "+")
int2
Harry is blue.
("Harry" "is" "blue" "+")
((triple11) -> (rule8 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
((triple12) -> (rule5 % int1))
Harry is blue.
("Harry" "is" "blue" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((((triple11) -> (rule8 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2
((((triple12) -> (rule5 % int2))) -> (rule4 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is blue.
("Harry" "is" "blue" "+")
int2