Bob is rough. Fiona is smart. Harry is nice. If someone is rough then they are green. Green, white people are red. Rough people are smart. If Harry is green and Harry is rough then Harry is white. All white, smart people are furry. Rough people are green. If someone is green then they are white. Green people are red.
Bob is rough.
("Bob" "is" "rough" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Harry is nice.
("Harry" "is" "nice" "+")
If someone is rough then they are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
Green, white people are red.
((("someone" "is" "green" "+") ("someone" "is" "white" "+")) -> ("someone" "is" "red" "+"))
Rough people are smart.
((("someone" "is" "rough" "+")) -> ("someone" "is" "smart" "+"))
If Harry is green and Harry is rough then Harry is white.
((("Harry" "is" "green" "+") ("Harry" "is" "rough" "+")) -> ("Harry" "is" "white" "+"))
All white, smart people are furry.
((("someone" "is" "white" "+") ("someone" "is" "smart" "+")) -> ("someone" "is" "furry" "+"))
Rough people are green.
((("someone" "is" "rough" "+")) -> ("someone" "is" "green" "+"))
If someone is green then they are white.
((("someone" "is" "green" "+")) -> ("someone" "is" "white" "+"))
Green people are red.
((("someone" "is" "green" "+")) -> ("someone" "is" "red" "+"))
Fiona is smart.
True
1
proof
[(triple2)]
("Fiona" "is" "smart" "+")
triple2
Harry is not nice.
False
1
inv-proof
[(triple3)]
("Harry" "is" "nice" "-")
triple3
Bob is green.
True
2
proof
[(((triple1) -> rule1) OR ((triple1) -> rule6))]
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is not green.
False
2
inv-proof
[(((triple1) -> rule1) OR ((triple1) -> rule6))]
("Bob" "is" "green" "-")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is white.
True
3
proof
[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule6)) -> rule7))]
("Bob" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is not red.
False
3
inv-proof
[(((((triple1) -> rule1)) -> rule8) OR ((((triple1) -> rule6)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule7)) -> rule2) OR ((((triple1) -> rule1) ((((triple1) -> rule6)) -> rule7)) -> rule2) OR ((((triple1) -> rule6) ((((triple1) -> rule1)) -> rule7)) -> rule2) OR ((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule2))]
("Bob" "is" "red" "-")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is furry.
True
6
proof
[(((((((triple1) -> rule1)) -> rule7) ((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule6)) -> rule7) ((triple1) -> rule3)) -> rule5))]
("Bob" "is" "furry" "+")
((((((triple1) -> (rule1 % int4))) -> (rule7 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((triple1) -> (rule6 % int4))) -> (rule7 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Bob is not furry.
False
6
inv-proof
[(((((((triple1) -> rule1)) -> rule7) ((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule6)) -> rule7) ((triple1) -> rule3)) -> rule5))]
("Bob" "is" "furry" "-")
((((((triple1) -> (rule1 % int4))) -> (rule7 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((triple1) -> (rule6 % int4))) -> (rule7 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
Fiona is not green.
Unknown
inv-rconc
[@1: Fiona is green.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "green" "-")
Harry is smart.
Unknown
rconc
[@1: Harry is smart.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "smart" "+")
Harry is not furry.
Unknown
inv-rconc
[@2: Harry is furry.[CWA. Example of deepest failure = (rule5 <- rule3 <- FAIL)]]
("Harry" "is" "furry" "-")
Fiona is furry.
Unknown
rconc
[@3: Fiona is furry.[CWA. Example of deepest failure = (rule5 <- rule7 <- rule1 <- FAIL)]]
("Fiona" "is" "furry" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Fiona is nice.
Unknown
random
[@0: Fiona is nice.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "nice" "+")
Bob is not nice.
Unknown
inv-random
[@0: Bob is nice.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "nice" "-")
Harry is rough.
Unknown
random
[@0: Harry is rough.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "rough" "+")
@0: Bob is rough.[(triple1)] Fiona is smart.[(triple2)] Harry is nice.[(triple3)] @1: Bob is green.[(((triple1) -> rule1) OR ((triple1) -> rule6))] Bob is smart.[(((triple1) -> rule3))] @2: Bob is red.[(((((triple1) -> rule1)) -> rule8) OR ((((triple1) -> rule6)) -> rule8) OR ((((triple1) -> rule1) ((((triple1) -> rule1)) -> rule7)) -> rule2) OR ((((triple1) -> rule1) ((((triple1) -> rule6)) -> rule7)) -> rule2) OR ((((triple1) -> rule6) ((((triple1) -> rule1)) -> rule7)) -> rule2) OR ((((triple1) -> rule6) ((((triple1) -> rule6)) -> rule7)) -> rule2))] Bob is white.[(((((triple1) -> rule1)) -> rule7) OR ((((triple1) -> rule6)) -> rule7))] @3: Bob is furry.[(((((((triple1) -> rule1)) -> rule7) ((triple1) -> rule3)) -> rule5) OR ((((((triple1) -> rule6)) -> rule7) ((triple1) -> rule3)) -> rule5))]
Bob is rough.
("Bob" "is" "rough" "+")
triple1
Fiona is smart.
("Fiona" "is" "smart" "+")
triple2
Harry is nice.
("Harry" "is" "nice" "+")
triple3
Bob is green.
("Bob" "is" "green" "+")
((triple1) -> (rule1 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
((triple1) -> (rule6 % int1))
Bob is green.
("Bob" "is" "green" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
((triple1) -> (rule3 % int1))
Bob is smart.
("Bob" "is" "smart" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
((((triple1) -> (rule1 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule8 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule1 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule1 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
((((triple1) -> (rule6 % int3)) ((((triple1) -> (rule6 % int3))) -> (rule7 % int2))) -> (rule2 % int1))
Bob is red.
("Bob" "is" "red" "+")
int1
Bob is white.
("Bob" "is" "white" "+")
int2
Bob is green.
("Bob" "is" "green" "+")
int3
Bob is white.
("Bob" "is" "white" "+")
((((triple1) -> (rule1 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
((((triple1) -> (rule6 % int2))) -> (rule7 % int1))
Bob is white.
("Bob" "is" "white" "+")
int1
Bob is green.
("Bob" "is" "green" "+")
int2
Bob is furry.
("Bob" "is" "furry" "+")
((((((triple1) -> (rule1 % int4))) -> (rule7 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4
((((((triple1) -> (rule6 % int4))) -> (rule7 % int3)) ((triple1) -> (rule3 % int2))) -> (rule5 % int1))
Bob is furry.
("Bob" "is" "furry" "+")
int1
Bob is smart.
("Bob" "is" "smart" "+")
int2
Bob is white.
("Bob" "is" "white" "+")
int3
Bob is green.
("Bob" "is" "green" "+")
int4