Bob is blue. Bob is nice. Charlie is furry. Fiona is big. Fiona is blue. Fiona is not green. Fiona is rough. Harry is big. Harry is green. Harry is nice. Harry is rough. Harry is white. If someone is furry then they are blue. If someone is green and not blue then they are nice. If someone is nice and not blue then they are not big. Nice people are big. Big people are white. White people are rough. If Charlie is white then Charlie is not rough. If Harry is big then Harry is nice.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is nice.
("Bob" "is" "nice" "+")
Charlie is furry.
("Charlie" "is" "furry" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Fiona is not green.
("Fiona" "is" "green" "-")
Fiona is rough.
("Fiona" "is" "rough" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is green.
("Harry" "is" "green" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is furry then they are blue.
((("someone" "is" "furry" "+")) -> ("someone" "is" "blue" "+"))
If someone is green and not blue then they are nice.
((("someone" "is" "green" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "nice" "+"))
If someone is nice and not blue then they are not big.
((("someone" "is" "nice" "+") ("someone" "is" "blue" "~")) -> ("someone" "is" "big" "-"))
Nice people are big.
((("someone" "is" "nice" "+")) -> ("someone" "is" "big" "+"))
Big people are white.
((("someone" "is" "big" "+")) -> ("someone" "is" "white" "+"))
White people are rough.
((("someone" "is" "white" "+")) -> ("someone" "is" "rough" "+"))
If Charlie is white then Charlie is not rough.
((("Charlie" "is" "white" "+")) -> ("Charlie" "is" "rough" "-"))
If Harry is big then Harry is nice.
((("Harry" "is" "big" "+")) -> ("Harry" "is" "nice" "+"))
Fiona is not green.
True
1
proof
[(triple6)]
("Fiona" "is" "green" "-")
triple6
Fiona is not big.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "big" "-")
triple4
Bob is big.
True
2
proof
[(((triple2) -> rule4))]
("Bob" "is" "big" "+")
((triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Fiona is not white.
False
2
inv-proof
[(((triple4) -> rule5))]
("Fiona" "is" "white" "-")
((triple4) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is white.
True
3
proof
[(((((triple2) -> rule4)) -> rule5))]
("Bob" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is not white.
False
3
inv-proof
[(((((triple2) -> rule4)) -> rule5))]
("Bob" "is" "white" "-")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
True
4
proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule6))]
("Bob" "is" "rough" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Bob is not rough.
False
4
inv-proof
[(((((((triple2) -> rule4)) -> rule5)) -> rule6))]
("Bob" "is" "rough" "-")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3
Fiona is not nice.
Unknown
inv-rconc
[@1: Fiona is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Fiona" "is" "nice" "-")
Charlie is white.
Unknown
rconc
[@3: Charlie is white.[CWA. Example of deepest failure = (rule5 <- rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "white" "+")
Charlie is not nice.
Unknown
inv-rconc
[@1: Charlie is nice.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Charlie" "is" "nice" "-")
Charlie is big.
Unknown
rconc
[@2: Charlie is big.[CWA. Example of deepest failure = (rule4 <- rule2 <- FAIL)]]
("Charlie" "is" "big" "+")
Harry is not furry.
Unknown
inv-random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "-")
Charlie is green.
Unknown
random
[@0: Charlie is green.[CWA. Example of deepest failure = (FAIL)]]
("Charlie" "is" "green" "+")
Bob is not furry.
Unknown
inv-random
[@0: Bob is furry.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "furry" "-")
Bob is green.
Unknown
random
[@0: Bob is green.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "green" "+")
@0: Bob is blue.[(triple1)] Bob is nice.[(triple2)] Charlie is furry.[(triple3)] Fiona is big.[(triple4)] Fiona is blue.[(triple5)] Fiona is not green.[(triple6)] Fiona is rough.[(triple7 OR ((((triple4) -> rule5)) -> rule6))] Harry is big.[(triple8 OR ((triple10) -> rule4))] Harry is green.[(triple9)] Harry is nice.[(triple10 OR ((triple8) -> rule8))] Harry is rough.[(triple11 OR ((triple12) -> rule6) OR ((((triple8) -> rule5)) -> rule6) OR ((((((triple10) -> rule4)) -> rule5)) -> rule6))] Harry is white.[(triple12 OR ((triple8) -> rule5) OR ((((triple10) -> rule4)) -> rule5))] @1: Bob is big.[(((triple2) -> rule4))] Charlie is blue.[(((triple3) -> rule1))] Fiona is white.[(((triple4) -> rule5))] @2: Bob is white.[(((((triple2) -> rule4)) -> rule5))] @3: Bob is rough.[(((((((triple2) -> rule4)) -> rule5)) -> rule6))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is nice.
("Bob" "is" "nice" "+")
triple2
Charlie is furry.
("Charlie" "is" "furry" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is blue.
("Fiona" "is" "blue" "+")
triple5
Fiona is not green.
("Fiona" "is" "green" "-")
triple6
Fiona is rough.
("Fiona" "is" "rough" "+")
triple7
((((triple4) -> (rule5 % int2))) -> (rule6 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
triple8
((triple10) -> (rule4 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
("Harry" "is" "green" "+")
triple9
Harry is nice.
("Harry" "is" "nice" "+")
triple10
((triple8) -> (rule8 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple11
((triple12) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple8) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
((((((triple10) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is white.
("Harry" "is" "white" "+")
triple12
((triple8) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
((((triple10) -> (rule4 % int2))) -> (rule5 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
((triple2) -> (rule4 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Charlie is blue.
("Charlie" "is" "blue" "+")
((triple3) -> (rule1 % int1))
Charlie is blue.
("Charlie" "is" "blue" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
((triple4) -> (rule5 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
((((triple2) -> (rule4 % int2))) -> (rule5 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((((triple2) -> (rule4 % int3))) -> (rule5 % int2))) -> (rule6 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is big.
("Bob" "is" "big" "+")
int3