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