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