Dave is green. Dave is red. Fiona is red. Fiona is smart. Gary is rough. Harry is cold. Harry is smart. Smart, big things are rough. All rough, cold things are white. All cold things are big.
Dave is green.
("Dave" "is" "green" "+")
Dave is red.
("Dave" "is" "red" "+")
Fiona is red.
("Fiona" "is" "red" "+")
Fiona is smart.
("Fiona" "is" "smart" "+")
Gary is rough.
("Gary" "is" "rough" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Smart, big things are rough.
((("something" "is" "smart" "+") ("something" "is" "big" "+")) -> ("something" "is" "rough" "+"))
All rough, cold things are white.
((("something" "is" "rough" "+") ("something" "is" "cold" "+")) -> ("something" "is" "white" "+"))
All cold things are big.
((("something" "is" "cold" "+")) -> ("something" "is" "big" "+"))
Dave is green.
True
1
proof
[(triple1)]
("Dave" "is" "green" "+")
triple1
Fiona is not smart.
False
1
inv-proof
[(triple4)]
("Fiona" "is" "smart" "-")
triple4
Harry is big.
True
2
proof
[(((triple6) -> rule3))]
("Harry" "is" "big" "+")
((triple6) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is not big.
False
2
inv-proof
[(((triple6) -> rule3))]
("Harry" "is" "big" "-")
((triple6) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
True
4
proof
[(((triple7 ((triple6) -> rule3)) -> rule1))]
("Harry" "is" "rough" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is not rough.
False
4
inv-proof
[(((triple7 ((triple6) -> rule3)) -> rule1))]
("Harry" "is" "rough" "-")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
True
6
proof
[(((((triple7 ((triple6) -> rule3)) -> rule1) triple6) -> rule2))]
("Harry" "is" "white" "+")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Harry is not white.
False
6
inv-proof
[(((((triple7 ((triple6) -> rule3)) -> rule1) triple6) -> rule2))]
("Harry" "is" "white" "-")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3
Gary is not white.
Unknown
inv-rconc
[@1: Gary is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Gary" "is" "white" "-")
Dave is white.
Unknown
rconc
[@1: Dave is white.[CWA. Example of deepest failure = (rule2 <- FAIL)]]
("Dave" "is" "white" "+")
Fiona is not big.
Unknown
inv-rconc
[@1: Fiona is big.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Fiona" "is" "big" "-")
Dave is rough.
Unknown
rconc
[@1: Dave is rough.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Dave" "is" "rough" "+")
Fiona is not cold.
Unknown
inv-random
[@0: Fiona is cold.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "cold" "-")
Harry is red.
Unknown
random
[@0: Harry is red.[CWA. Example of deepest failure = (FAIL)]]
("Harry" "is" "red" "+")
Gary is not red.
Unknown
inv-random
[@0: Gary is red.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "red" "-")
Gary is cold.
Unknown
random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "+")
@0: Dave is green.[(triple1)] Dave is red.[(triple2)] Fiona is red.[(triple3)] Fiona is smart.[(triple4)] Gary is rough.[(triple5)] Harry is cold.[(triple6)] Harry is smart.[(triple7)] @1: Harry is big.[(((triple6) -> rule3))] @2: Harry is rough.[(((triple7 ((triple6) -> rule3)) -> rule1))] @3: Harry is white.[(((((triple7 ((triple6) -> rule3)) -> rule1) triple6) -> rule2))]
Dave is green.
("Dave" "is" "green" "+")
triple1
Dave is red.
("Dave" "is" "red" "+")
triple2
Fiona is red.
("Fiona" "is" "red" "+")
triple3
Fiona is smart.
("Fiona" "is" "smart" "+")
triple4
Gary is rough.
("Gary" "is" "rough" "+")
triple5
Harry is cold.
("Harry" "is" "cold" "+")
triple6
Harry is smart.
("Harry" "is" "smart" "+")
triple7
Harry is big.
("Harry" "is" "big" "+")
((triple6) -> (rule3 % int1))
Harry is big.
("Harry" "is" "big" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
((triple7 ((triple6) -> (rule3 % int2))) -> (rule1 % int1))
Harry is rough.
("Harry" "is" "rough" "+")
int1
Harry is big.
("Harry" "is" "big" "+")
int2
Harry is white.
("Harry" "is" "white" "+")
((((triple7 ((triple6) -> (rule3 % int3))) -> (rule1 % int2)) triple6) -> (rule2 % int1))
Harry is white.
("Harry" "is" "white" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
int2
Harry is big.
("Harry" "is" "big" "+")
int3