Bob is blue. Bob is furry. Bob is green. Bob is rough. Erin is furry. Fiona is blue. Harry is white. If someone is green then they are white. If someone is white then they are big. If Fiona is rough then Fiona is white. If Erin is big then Erin is blue. If someone is blue then they are rough. If Fiona is furry then Fiona is blue. Furry people are green. If someone is big and white then they are green. Green, red people are blue.
Bob is blue.
("Bob" "is" "blue" "+")
Bob is furry.
("Bob" "is" "furry" "+")
Bob is green.
("Bob" "is" "green" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Erin is furry.
("Erin" "is" "furry" "+")
Fiona is blue.
("Fiona" "is" "blue" "+")
Harry is white.
("Harry" "is" "white" "+")
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
If someone is white then they are big.
((("someone" "is" "white" "+")) -> ("someone" "is" "big" "+"))
If Fiona is rough then Fiona is white.
((("Fiona" "is" "rough" "+")) -> ("Fiona" "is" "white" "+"))
If Erin is big then Erin is blue.
((("Erin" "is" "big" "+")) -> ("Erin" "is" "blue" "+"))
If someone is blue then they are rough.
((("someone" "is" "blue" "+")) -> ("someone" "is" "rough" "+"))
If Fiona is furry then Fiona is blue.
((("Fiona" "is" "furry" "+")) -> ("Fiona" "is" "blue" "+"))
Furry people are green.
((("someone" "is" "furry" "+")) -> ("someone" "is" "green" "+"))
If someone is big and white then they are green.
((("someone" "is" "big" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "green" "+"))
Green, red people are blue.
((("someone" "is" "green" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "blue" "+"))
Bob is rough.
True
1
proof
[(triple4 OR ((triple1) -> rule5))]
("Bob" "is" "rough" "+")
triple4
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is not green.
False
1
inv-proof
[(triple3 OR ((triple2) -> rule7))]
("Bob" "is" "green" "-")
triple3
((triple2) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Erin is green.
True
2
proof
[(((triple5) -> rule7))]
("Erin" "is" "green" "+")
((triple5) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple7) -> rule2))]
("Harry" "is" "big" "-")
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is green.
True
4
proof
[(((((triple7) -> rule2) triple7) -> rule8))]
("Harry" "is" "green" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Bob is not big.
False
3
inv-proof
[(((((triple3) -> rule1)) -> rule2) OR ((((((triple2) -> rule7)) -> rule1)) -> rule2))]
("Bob" "is" "big" "-")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Fiona is big.
True
4
proof
[(((((((triple6) -> rule5)) -> rule3)) -> rule2))]
("Fiona" "is" "big" "+")
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Fiona is not big.
False
4
inv-proof
[(((((((triple6) -> rule5)) -> rule3)) -> rule2))]
("Fiona" "is" "big" "-")
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Erin is blue.
True
5
proof
[(((((((((triple5) -> rule7)) -> rule1)) -> rule2)) -> rule4))]
("Erin" "is" "blue" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Fiona is not green.
False
8
inv-proof
[(((((((((triple6) -> rule5)) -> rule3)) -> rule2) ((((triple6) -> rule5)) -> rule3)) -> rule8))]
("Fiona" "is" "green" "-")
((((((((triple6) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) ((((triple6) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Erin is rough.
True
6
proof
[(((((((((((triple5) -> rule7)) -> rule1)) -> rule2)) -> rule4)) -> rule5))]
("Erin" "is" "rough" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Erin is not rough.
False
6
inv-proof
[(((((((((((triple5) -> rule7)) -> rule1)) -> rule2)) -> rule4)) -> rule5))]
("Erin" "is" "rough" "-")
((((((((((triple5) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5
Harry is not rough.
Unknown
inv-rconc
[@2: Harry is rough.[CWA. Example of deepest failure = (rule5 <- rule9 <- FAIL)]]
("Harry" "is" "rough" "-")
Harry is blue.
Unknown
rconc
[@1: Harry is blue.[CWA. Example of deepest failure = (rule9 <- FAIL)]]
("Harry" "is" "blue" "+")
Erin is not red.
Unknown
inv-random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Harry is not red.
Unknown
inv-random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "-")
Bob is red.
Unknown
random
[@0: Bob is red.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "red" "+")
Fiona is not furry.
Unknown
inv-random
[@0: Fiona is furry.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "furry" "-")
Harry is furry.
Unknown
random
[@0: Harry is furry.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "furry" "+")
@0: Bob is blue.[(triple1)] Bob is furry.[(triple2)] Bob is green.[(triple3 OR ((triple2) -> rule7))] Bob is rough.[(triple4 OR ((triple1) -> rule5))] Erin is furry.[(triple5)] Fiona is blue.[(triple6)] Harry is white.[(triple7)] @1: Bob is white.[(((triple3) -> rule1) OR ((((triple2) -> rule7)) -> rule1))] Erin is green.[(((triple5) -> rule7))] Fiona is rough.[(((triple6) -> rule5))] Harry is big.[(((triple7) -> rule2))] @2: Bob is big.[(((((triple3) -> rule1)) -> rule2) OR ((((((triple2) -> rule7)) -> rule1)) -> rule2))] Erin is white.[(((((triple5) -> rule7)) -> rule1))] Fiona is white.[(((((triple6) -> rule5)) -> rule3))] Harry is green.[(((((triple7) -> rule2) triple7) -> rule8))] @3: Erin is big.[(((((((triple5) -> rule7)) -> rule1)) -> rule2))] Fiona is big.[(((((((triple6) -> rule5)) -> rule3)) -> rule2))] @4: Erin is blue.[(((((((((triple5) -> rule7)) -> rule1)) -> rule2)) -> rule4))] Fiona is green.[(((((((((triple6) -> rule5)) -> rule3)) -> rule2) ((((triple6) -> rule5)) -> rule3)) -> rule8))] @5: Erin is rough.[(((((((((((triple5) -> rule7)) -> rule1)) -> rule2)) -> rule4)) -> rule5))]
Bob is blue.
("Bob" "is" "blue" "+")
triple1
Bob is furry.
("Bob" "is" "furry" "+")
triple2
Bob is green.
("Bob" "is" "green" "+")
triple3
((triple2) -> (rule7 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
triple4
((triple1) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Erin is furry.
("Erin" "is" "furry" "+")
triple5
Fiona is blue.
("Fiona" "is" "blue" "+")
triple6
Harry is white.
("Harry" "is" "white" "+")
triple7
Bob is white.
("Bob" "is" "white" "+")
((triple3) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
((((triple2) -> (rule7 % int2))) -> (rule1 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
((triple5) -> (rule7 % int1))
Erin is green.
("Erin" "is" "green" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple6) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
((triple7) -> (rule2 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((((triple3) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
((((((triple2) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
((((triple5) -> (rule7 % int2))) -> (rule1 % int1))
Erin is white.
("Erin" "is" "white" "+")
int1
Erin is green.
("Erin" "is" "green" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
((((triple6) -> (rule5 % int2))) -> (rule3 % int1))
Fiona is white.
("Fiona" "is" "white" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
int2
Harry is green.
("Harry" "is" "green" "+")
((((triple7) -> (rule2 % int2)) triple7) -> (rule8 % int1))
Harry is green.
("Harry" "is" "green" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
((((((triple5) -> (rule7 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Erin is white.
("Erin" "is" "white" "+")
int2
Erin is green.
("Erin" "is" "green" "+")
int3
Fiona is big.
("Fiona" "is" "big" "+")
((((((triple6) -> (rule5 % int3))) -> (rule3 % int2))) -> (rule2 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
int2
Fiona is rough.
("Fiona" "is" "rough" "+")
int3
Erin is blue.
("Erin" "is" "blue" "+")
((((((((triple5) -> (rule7 % int4))) -> (rule1 % int3))) -> (rule2 % int2))) -> (rule4 % int1))
Erin is blue.
("Erin" "is" "blue" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is white.
("Erin" "is" "white" "+")
int3
Erin is green.
("Erin" "is" "green" "+")
int4
Fiona is green.
("Fiona" "is" "green" "+")
((((((((triple6) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule2 % int2)) ((((triple6) -> (rule5 % int4))) -> (rule3 % int3))) -> (rule8 % int1))
Fiona is green.
("Fiona" "is" "green" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is white.
("Fiona" "is" "white" "+")
int3
Fiona is rough.
("Fiona" "is" "rough" "+")
int4
Erin is rough.
("Erin" "is" "rough" "+")
((((((((((triple5) -> (rule7 % int5))) -> (rule1 % int4))) -> (rule2 % int3))) -> (rule4 % int2))) -> (rule5 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is blue.
("Erin" "is" "blue" "+")
int2
Erin is big.
("Erin" "is" "big" "+")
int3
Erin is white.
("Erin" "is" "white" "+")
int4
Erin is green.
("Erin" "is" "green" "+")
int5