Anne is quiet. Anne is red. Anne is white. Bob is cold. Bob is quiet. Bob is red. Bob is rough. Bob is young. Fiona is big. Harry is big. Harry is cold. Harry is quiet. Harry is red. Harry is rough. Harry is white. Harry is young. If something is young then it is big. Big things are cold. If something is quiet then it is young.
Anne is quiet.
("Anne" "is" "quiet" "+")
Anne is red.
("Anne" "is" "red" "+")
Anne is white.
("Anne" "is" "white" "+")
Bob is cold.
("Bob" "is" "cold" "+")
Bob is quiet.
("Bob" "is" "quiet" "+")
Bob is red.
("Bob" "is" "red" "+")
Bob is rough.
("Bob" "is" "rough" "+")
Bob is young.
("Bob" "is" "young" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is quiet.
("Harry" "is" "quiet" "+")
Harry is red.
("Harry" "is" "red" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is young then it is big.
((("something" "is" "young" "+")) -> ("something" "is" "big" "+"))
Big things are cold.
((("something" "is" "big" "+")) -> ("something" "is" "cold" "+"))
If something is quiet then it is young.
((("something" "is" "quiet" "+")) -> ("something" "is" "young" "+"))
Fiona is big.
True
1
proof
[(triple9)]
("Fiona" "is" "big" "+")
triple9
Bob is not young.
False
1
inv-proof
[(triple8 OR ((triple5) -> rule3))]
("Bob" "is" "young" "-")
triple8
((triple5) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is big.
True
2
proof
[(((triple8) -> rule1) OR ((((triple5) -> rule3)) -> rule1))]
("Bob" "is" "big" "+")
((triple8) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Anne is not young.
False
2
inv-proof
[(((triple1) -> rule3))]
("Anne" "is" "young" "-")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Anne is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Anne" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
True
4
proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Anne" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Anne is not cold.
False
4
inv-proof
[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
("Anne" "is" "cold" "-")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3
Fiona is not young.
Unknown
inv-rconc
[@1: Fiona is young.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "young" "-")
Fiona is white.
Unknown
random
[@0: Fiona is white.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "white" "+")
Fiona is not quiet.
Unknown
inv-random
[@0: Fiona is quiet.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "quiet" "-")
Fiona is red.
Unknown
random
[@0: Fiona is red.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "red" "+")
Anne is not rough.
Unknown
inv-random
[@0: Anne is rough.[CWA. Example of deepest failure = (FAIL)]]
("Anne" "is" "rough" "-")
Bob is white.
Unknown
random
[@0: Bob is white.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "white" "+")
@0: Anne is quiet.[(triple1)] Anne is red.[(triple2)] Anne is white.[(triple3)] Bob is cold.[(triple4 OR ((((triple8) -> rule1)) -> rule2) OR ((((((triple5) -> rule3)) -> rule1)) -> rule2))] Bob is quiet.[(triple5)] Bob is red.[(triple6)] Bob is rough.[(triple7)] Bob is young.[(triple8 OR ((triple5) -> rule3))] Fiona is big.[(triple9)] Harry is big.[(triple10 OR ((triple16) -> rule1) OR ((((triple12) -> rule3)) -> rule1))] Harry is cold.[(triple11 OR ((triple10) -> rule2) OR ((((triple16) -> rule1)) -> rule2) OR ((((((triple12) -> rule3)) -> rule1)) -> rule2))] Harry is quiet.[(triple12)] Harry is red.[(triple13)] Harry is rough.[(triple14)] Harry is white.[(triple15)] Harry is young.[(triple16 OR ((triple12) -> rule3))] @1: Anne is young.[(((triple1) -> rule3))] Bob is big.[(((triple8) -> rule1) OR ((((triple5) -> rule3)) -> rule1))] Fiona is cold.[(((triple9) -> rule2))] @2: Anne is big.[(((((triple1) -> rule3)) -> rule1))] @3: Anne is cold.[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
Anne is quiet.
("Anne" "is" "quiet" "+")
triple1
Anne is red.
("Anne" "is" "red" "+")
triple2
Anne is white.
("Anne" "is" "white" "+")
triple3
Bob is cold.
("Bob" "is" "cold" "+")
triple4
((((triple8) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
((((((triple5) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
int3
Bob is quiet.
("Bob" "is" "quiet" "+")
triple5
Bob is red.
("Bob" "is" "red" "+")
triple6
Bob is rough.
("Bob" "is" "rough" "+")
triple7
Bob is young.
("Bob" "is" "young" "+")
triple8
((triple5) -> (rule3 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Fiona is big.
("Fiona" "is" "big" "+")
triple9
Harry is big.
("Harry" "is" "big" "+")
triple10
((triple16) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
((((triple12) -> (rule3 % int2))) -> (rule1 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is young.
("Harry" "is" "young" "+")
int2
Harry is cold.
("Harry" "is" "cold" "+")
triple11
((triple10) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple16) -> (rule1 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
((((((triple12) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is young.
("Harry" "is" "young" "+")
int3
Harry is quiet.
("Harry" "is" "quiet" "+")
triple12
Harry is red.
("Harry" "is" "red" "+")
triple13
Harry is rough.
("Harry" "is" "rough" "+")
triple14
Harry is white.
("Harry" "is" "white" "+")
triple15
Harry is young.
("Harry" "is" "young" "+")
triple16
((triple12) -> (rule3 % int1))
Harry is young.
("Harry" "is" "young" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
((triple1) -> (rule3 % int1))
Anne is young.
("Anne" "is" "young" "+")
int1
Bob is big.
("Bob" "is" "big" "+")
((triple8) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
((((triple5) -> (rule3 % int2))) -> (rule1 % int1))
Bob is big.
("Bob" "is" "big" "+")
int1
Bob is young.
("Bob" "is" "young" "+")
int2
Fiona is cold.
("Fiona" "is" "cold" "+")
((triple9) -> (rule2 % int1))
Fiona is cold.
("Fiona" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Anne is big.
("Anne" "is" "big" "+")
int1
Anne is young.
("Anne" "is" "young" "+")
int2
Anne is cold.
("Anne" "is" "cold" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Anne is cold.
("Anne" "is" "cold" "+")
int1
Anne is big.
("Anne" "is" "big" "+")
int2
Anne is young.
("Anne" "is" "young" "+")
int3