Bob is big. Bob is cold. Bob is red. Bob is round. Bob is young. Erin is quiet. Erin is rough. Erin is round. Fiona is big. Fiona is cold. Fiona is quiet. Fiona is rough. Fiona is round. Fiona is young. Harry is big. Quiet people are big. Big people are rough. If someone is young and red then they are round. All young people are round. If someone is red then they are cold. All red people are quiet. Red people are rough. If Harry is rough and Harry is big then Harry is red.
Bob is big.
("Bob" "is" "big" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is round.
("Bob" "is" "round" "+")
Bob is young.
("Bob" "is" "young" "+")
Erin is quiet.
("Erin" "is" "quiet" "+")
Erin is rough.
("Erin" "is" "rough" "+")
Erin is round.
("Erin" "is" "round" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is cold.
("Fiona" "is" "cold" "+")
Fiona is quiet.
("Fiona" "is" "quiet" "+")
Fiona is rough.
("Fiona" "is" "rough" "+")
Fiona is round.
("Fiona" "is" "round" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Quiet people are big.
((("someone" "is" "quiet" "+")) -> ("someone" "is" "big" "+"))
Big people are rough.
((("someone" "is" "big" "+")) -> ("someone" "is" "rough" "+"))
If someone is young and red then they are round.
((("someone" "is" "young" "+") ("someone" "is" "red" "+")) -> ("someone" "is" "round" "+"))
All young people are round.
((("someone" "is" "young" "+")) -> ("someone" "is" "round" "+"))
If someone is red then they are cold.
((("someone" "is" "red" "+")) -> ("someone" "is" "cold" "+"))
All red people are quiet.
((("someone" "is" "red" "+")) -> ("someone" "is" "quiet" "+"))
Red people are rough.
((("someone" "is" "red" "+")) -> ("someone" "is" "rough" "+"))
If Harry is rough and Harry is big then Harry is red.
((("Harry" "is" "rough" "+") ("Harry" "is" "big" "+")) -> ("Harry" "is" "red" "+"))
Fiona is big.
True
1
proof
[(triple9 OR ((triple11) -> rule1))]
("Fiona" "is" "big" "+")
triple9
((triple11) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Bob is not young.
False
1
inv-proof
[(triple5)]
("Bob" "is" "young" "-")
triple5
Erin is big.
True
2
proof
[(((triple6) -> rule1))]
("Erin" "is" "big" "+")
((triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Bob is not quiet.
False
2
inv-proof
[(((triple3) -> rule6))]
("Bob" "is" "quiet" "-")
((triple3) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Harry is red.
True
4
proof
[(((((triple15) -> rule2) triple15) -> rule8))]
("Harry" "is" "red" "+")
((((triple15) -> (rule2 % int2)) triple15) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is not red.
False
4
inv-proof
[(((((triple15) -> rule2) triple15) -> rule8))]
("Harry" "is" "red" "-")
((((triple15) -> (rule2 % int2)) triple15) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
True
5
proof
[(((((((triple15) -> rule2) triple15) -> rule8)) -> rule5))]
("Harry" "is" "cold" "+")
((((((triple15) -> (rule2 % int3)) triple15) -> (rule8 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is not quiet.
False
5
inv-proof
[(((((((triple15) -> rule2) triple15) -> rule8)) -> rule6))]
("Harry" "is" "quiet" "-")
((((((triple15) -> (rule2 % int3)) triple15) -> (rule8 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Erin is not cold.
Unknown
inv-rconc
[@1: Erin is cold.[CWA. Example of deepest failure = (rule5 <- FAIL)]]
("Erin" "is" "cold" "-")
Harry is round.
Unknown
rconc
[@1: Harry is round.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Harry" "is" "round" "+")
Erin is not young.
Unknown
inv-random
[@0: Erin is young.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "young" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Harry is not young.
Unknown
inv-random
[@0: Harry is young.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "young" "-")
Erin is red.
Unknown
random
[@0: Erin is red.[CWA. Example of deepest failure = (FAIL)]]
("Erin" "is" "red" "+")
@0: Bob is big.[(triple1 OR ((((triple3) -> rule6)) -> rule1))] Bob is cold.[(triple2 OR ((triple3) -> rule5))] Bob is red.[(triple3)] Bob is round.[(triple4 OR ((triple5) -> rule4) OR ((triple5 triple3) -> rule3))] Bob is young.[(triple5)] Erin is quiet.[(triple6)] Erin is rough.[(triple7 OR ((((triple6) -> rule1)) -> rule2))] Erin is round.[(triple8)] Fiona is big.[(triple9 OR ((triple11) -> rule1))] Fiona is cold.[(triple10)] Fiona is quiet.[(triple11)] Fiona is rough.[(triple12 OR ((triple9) -> rule2) OR ((((triple11) -> rule1)) -> rule2))] Fiona is round.[(triple13 OR ((triple14) -> rule4))] Fiona is young.[(triple14)] Harry is big.[(triple15)] @1: Bob is quiet.[(((triple3) -> rule6))] Bob is rough.[(((triple1) -> rule2) OR ((triple3) -> rule7) OR ((((((triple3) -> rule6)) -> rule1)) -> rule2))] Erin is big.[(((triple6) -> rule1))] Harry is rough.[(((triple15) -> rule2))] @2: Harry is red.[(((((triple15) -> rule2) triple15) -> rule8))] @3: Harry is cold.[(((((((triple15) -> rule2) triple15) -> rule8)) -> rule5))] Harry is quiet.[(((((((triple15) -> rule2) triple15) -> rule8)) -> rule6))]
Bob is big.
("Bob" "is" "big" "+")
triple1
((((triple3) -> (rule6 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is quiet.
("Bob" "is" "quiet" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
triple2
((triple3) -> (rule5 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is red.
("Bob" "is" "red" "+")
triple3
Bob is round.
("Bob" "is" "round" "+")
triple4
((triple5) -> (rule4 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
((triple5 triple3) -> (rule3 % int1))
Bob is round.
("Bob" "is" "round" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
triple5
Erin is quiet.
("Erin" "is" "quiet" "+")
triple6
Erin is rough.
("Erin" "is" "rough" "+")
triple7
((((triple6) -> (rule1 % int2))) -> (rule2 % int1))
Erin is rough.
("Erin" "is" "rough" "+")
int1
Erin is big.
("Erin" "is" "big" "+")
int2
Erin is round.
("Erin" "is" "round" "+")
triple8
Fiona is big.
("Fiona" "is" "big" "+")
triple9
((triple11) -> (rule1 % int1))
Fiona is big.
("Fiona" "is" "big" "+")
int1
Fiona is cold.
("Fiona" "is" "cold" "+")
triple10
Fiona is quiet.
("Fiona" "is" "quiet" "+")
triple11
Fiona is rough.
("Fiona" "is" "rough" "+")
triple12
((triple9) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple11) -> (rule1 % int2))) -> (rule2 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
int2
Fiona is round.
("Fiona" "is" "round" "+")
triple13
((triple14) -> (rule4 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is young.
("Fiona" "is" "young" "+")
triple14
Harry is big.
("Harry" "is" "big" "+")
triple15
Bob is quiet.
("Bob" "is" "quiet" "+")
((triple3) -> (rule6 % int1))
Bob is quiet.
("Bob" "is" "quiet" "+")
int1
Bob is rough.
("Bob" "is" "rough" "+")
((triple1) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((triple3) -> (rule7 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
((((((triple3) -> (rule6 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is quiet.
("Bob" "is" "quiet" "+")
int3
Erin is big.
("Erin" "is" "big" "+")
((triple6) -> (rule1 % int1))
Erin is big.
("Erin" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple15) -> (rule2 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
((((triple15) -> (rule2 % int2)) triple15) -> (rule8 % int1))
Harry is red.
("Harry" "is" "red" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
((((((triple15) -> (rule2 % int3)) triple15) -> (rule8 % int2))) -> (rule5 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
((((((triple15) -> (rule2 % int3)) triple15) -> (rule8 % int2))) -> (rule6 % int1))
Harry is quiet.
("Harry" "is" "quiet" "+")
int1
Harry is red.
("Harry" "is" "red" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
int3