Bob is green. Bob is white. Fiona is nice. Fiona is white. Gary is green. Gary is young. Harry is blue. Harry is nice. Harry is white. Harry is young. If Harry is rough and Harry is green then Harry is young. If something is cold then it is young. If something is white then it is nice. If Bob is green and Bob is blue then Bob is white. If something is nice then it is rough. Nice, green things are cold.
Bob is green.
("Bob" "is" "green" "+")
Bob is white.
("Bob" "is" "white" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Fiona is white.
("Fiona" "is" "white" "+")
Gary is green.
("Gary" "is" "green" "+")
Gary is young.
("Gary" "is" "young" "+")
Harry is blue.
("Harry" "is" "blue" "+")
Harry is nice.
("Harry" "is" "nice" "+")
Harry is white.
("Harry" "is" "white" "+")
Harry is young.
("Harry" "is" "young" "+")
If Harry is rough and Harry is green then Harry is young.
((("Harry" "is" "rough" "+") ("Harry" "is" "green" "+")) -> ("Harry" "is" "young" "+"))
If something is cold then it is young.
((("something" "is" "cold" "+")) -> ("something" "is" "young" "+"))
If something is white then it is nice.
((("something" "is" "white" "+")) -> ("something" "is" "nice" "+"))
If Bob is green and Bob is blue then Bob is white.
((("Bob" "is" "green" "+") ("Bob" "is" "blue" "+")) -> ("Bob" "is" "white" "+"))
If something is nice then it is rough.
((("something" "is" "nice" "+")) -> ("something" "is" "rough" "+"))
Nice, green things are cold.
((("something" "is" "nice" "+") ("something" "is" "green" "+")) -> ("something" "is" "cold" "+"))
Harry is young.
True
1
proof
[(triple10)]
("Harry" "is" "young" "+")
triple10
Fiona is not white.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "white" "-")
triple4
Harry is rough.
True
2
proof
[(((triple8) -> rule5) OR ((((triple9) -> rule3)) -> rule5))]
("Harry" "is" "rough" "+")
((triple8) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Harry is not rough.
False
2
inv-proof
[(((triple8) -> rule5) OR ((((triple9) -> rule3)) -> rule5))]
("Harry" "is" "rough" "-")
((triple8) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is cold.
True
4
proof
[(((((triple2) -> rule3) triple1) -> rule6))]
("Bob" "is" "cold" "+")
((((triple2) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is not cold.
False
4
inv-proof
[(((((triple2) -> rule3) triple1) -> rule6))]
("Bob" "is" "cold" "-")
((((triple2) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
True
5
proof
[(((((((triple2) -> rule3) triple1) -> rule6)) -> rule2))]
("Bob" "is" "young" "+")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Bob is not young.
False
5
inv-proof
[(((((((triple2) -> rule3) triple1) -> rule6)) -> rule2))]
("Bob" "is" "young" "-")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3
Gary is not cold.
Unknown
inv-rconc
[@2: Gary is cold.[CWA. Example of deepest failure = (rule6 <- rule3 <- FAIL)]]
("Gary" "is" "cold" "-")
Fiona is young.
Unknown
rconc
[@2: Fiona is young.[CWA. Example of deepest failure = (rule2 <- rule6 <- FAIL)]]
("Fiona" "is" "young" "+")
Gary is not nice.
Unknown
inv-rconc
[@1: Gary is nice.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Gary" "is" "nice" "-")
Harry is cold.
Unknown
rconc
[@1: Harry is cold.[CWA. Example of deepest failure = (rule6 <- FAIL)]]
("Harry" "is" "cold" "+")
Fiona is not green.
Unknown
inv-random
[@0: Fiona is green.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "green" "-")
Bob is blue.
Unknown
random
[@0: Bob is blue.[CWA. Example of deepest failure = (FAIL)]]
("Bob" "is" "blue" "+")
Fiona is not blue.
Unknown
inv-random
[@0: Fiona is blue.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "blue" "-")
Gary is blue.
Unknown
random
[@0: Gary is blue.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "blue" "+")
@0: Bob is green.[(triple1)] Bob is white.[(triple2)] Fiona is nice.[(triple3 OR ((triple4) -> rule3))] Fiona is white.[(triple4)] Gary is green.[(triple5)] Gary is young.[(triple6)] Harry is blue.[(triple7)] Harry is nice.[(triple8 OR ((triple9) -> rule3))] Harry is white.[(triple9)] Harry is young.[(triple10)] @1: Bob is nice.[(((triple2) -> rule3))] Fiona is rough.[(((triple3) -> rule5) OR ((((triple4) -> rule3)) -> rule5))] Harry is rough.[(((triple8) -> rule5) OR ((((triple9) -> rule3)) -> rule5))] @2: Bob is cold.[(((((triple2) -> rule3) triple1) -> rule6))] Bob is rough.[(((((triple2) -> rule3)) -> rule5))] @3: Bob is young.[(((((((triple2) -> rule3) triple1) -> rule6)) -> rule2))]
Bob is green.
("Bob" "is" "green" "+")
triple1
Bob is white.
("Bob" "is" "white" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
((triple4) -> (rule3 % int1))
Fiona is nice.
("Fiona" "is" "nice" "+")
int1
Fiona is white.
("Fiona" "is" "white" "+")
triple4
Gary is green.
("Gary" "is" "green" "+")
triple5
Gary is young.
("Gary" "is" "young" "+")
triple6
Harry is blue.
("Harry" "is" "blue" "+")
triple7
Harry is nice.
("Harry" "is" "nice" "+")
triple8
((triple9) -> (rule3 % int1))
Harry is nice.
("Harry" "is" "nice" "+")
int1
Harry is white.
("Harry" "is" "white" "+")
triple9
Harry is young.
("Harry" "is" "young" "+")
triple10
Bob is nice.
("Bob" "is" "nice" "+")
((triple2) -> (rule3 % int1))
Bob is nice.
("Bob" "is" "nice" "+")
int1
Fiona is rough.
("Fiona" "is" "rough" "+")
((triple3) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
((((triple4) -> (rule3 % int2))) -> (rule5 % int1))
Fiona is rough.
("Fiona" "is" "rough" "+")
int1
Fiona is nice.
("Fiona" "is" "nice" "+")
int2
Harry is rough.
("Harry" "is" "rough" "+")
((triple8) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
((((triple9) -> (rule3 % int2))) -> (rule5 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is nice.
("Harry" "is" "nice" "+")
int2
Bob is cold.
("Bob" "is" "cold" "+")
((((triple2) -> (rule3 % int2)) triple1) -> (rule6 % int1))
Bob is cold.
("Bob" "is" "cold" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is rough.
("Bob" "is" "rough" "+")
((((triple2) -> (rule3 % int2))) -> (rule5 % int1))
Bob is rough.
("Bob" "is" "rough" "+")
int1
Bob is nice.
("Bob" "is" "nice" "+")
int2
Bob is young.
("Bob" "is" "young" "+")
((((((triple2) -> (rule3 % int3)) triple1) -> (rule6 % int2))) -> (rule2 % int1))
Bob is young.
("Bob" "is" "young" "+")
int1
Bob is cold.
("Bob" "is" "cold" "+")
int2
Bob is nice.
("Bob" "is" "nice" "+")
int3