Dave is rough. Erin is cold. Fiona is nice. Gary is smart. If something is furry then it is big. All big things are smart. If something is rough then it is furry.
Dave is rough.
("Dave" "is" "rough" "+")
Erin is cold.
("Erin" "is" "cold" "+")
Fiona is nice.
("Fiona" "is" "nice" "+")
Gary is smart.
("Gary" "is" "smart" "+")
If something is furry then it is big.
((("something" "is" "furry" "+")) -> ("something" "is" "big" "+"))
All big things are smart.
((("something" "is" "big" "+")) -> ("something" "is" "smart" "+"))
If something is rough then it is furry.
((("something" "is" "rough" "+")) -> ("something" "is" "furry" "+"))
Gary is smart.
True
1
proof
[(triple4)]
("Gary" "is" "smart" "+")
triple4
Erin is not cold.
False
1
inv-proof
[(triple2)]
("Erin" "is" "cold" "-")
triple2
Dave is furry.
True
2
proof
[(((triple1) -> rule3))]
("Dave" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is not furry.
False
2
inv-proof
[(((triple1) -> rule3))]
("Dave" "is" "furry" "-")
((triple1) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
True
3
proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is not big.
False
3
inv-proof
[(((((triple1) -> rule3)) -> rule1))]
("Dave" "is" "big" "-")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Erin is not furry.
Unknown
inv-rconc
[@1: Erin is furry.[CWA. Example of deepest failure = (rule3 <- FAIL)]]
("Erin" "is" "furry" "-")
Erin is big.
Unknown
rconc
[@2: Erin is big.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Erin" "is" "big" "+")
Fiona is not big.
Unknown
inv-rconc
[@2: Fiona is big.[CWA. Example of deepest failure = (rule1 <- rule3 <- FAIL)]]
("Fiona" "is" "big" "-")
Gary is round.
Unknown
random
[@0: Gary is round.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "round" "+")
Gary is not cold.
Unknown
inv-random
[@0: Gary is cold.[CWA. Example of deepest failure = (FAIL)]]
("Gary" "is" "cold" "-")
Fiona is round.
Unknown
random
[@0: Fiona is round.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "round" "+")
@0: Dave is rough.[(triple1)] Erin is cold.[(triple2)] Fiona is nice.[(triple3)] Gary is smart.[(triple4)] @1: Dave is furry.[(((triple1) -> rule3))] @2: Dave is big.[(((((triple1) -> rule3)) -> rule1))] @3: Dave is smart.[(((((((triple1) -> rule3)) -> rule1)) -> rule2))]
Dave is rough.
("Dave" "is" "rough" "+")
triple1
Erin is cold.
("Erin" "is" "cold" "+")
triple2
Fiona is nice.
("Fiona" "is" "nice" "+")
triple3
Gary is smart.
("Gary" "is" "smart" "+")
triple4
Dave is furry.
("Dave" "is" "furry" "+")
((triple1) -> (rule3 % int1))
Dave is furry.
("Dave" "is" "furry" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
((((triple1) -> (rule3 % int2))) -> (rule1 % int1))
Dave is big.
("Dave" "is" "big" "+")
int1
Dave is furry.
("Dave" "is" "furry" "+")
int2
Dave is smart.
("Dave" "is" "smart" "+")
((((((triple1) -> (rule3 % int3))) -> (rule1 % int2))) -> (rule2 % int1))
Dave is smart.
("Dave" "is" "smart" "+")
int1
Dave is big.
("Dave" "is" "big" "+")
int2
Dave is furry.
("Dave" "is" "furry" "+")
int3