Dave is big. Dave is kind. Dave is smart. Fiona is big. Fiona is young. Harry is big. Harry is cold. Harry is kind. Harry is rough. Harry is round. Harry is smart. Harry is young. If something is kind and smart then it is cold. All young, big things are kind. Kind things are round.
Dave is big.
("Dave" "is" "big" "+")
Dave is kind.
("Dave" "is" "kind" "+")
Dave is smart.
("Dave" "is" "smart" "+")
Fiona is big.
("Fiona" "is" "big" "+")
Fiona is young.
("Fiona" "is" "young" "+")
Harry is big.
("Harry" "is" "big" "+")
Harry is cold.
("Harry" "is" "cold" "+")
Harry is kind.
("Harry" "is" "kind" "+")
Harry is rough.
("Harry" "is" "rough" "+")
Harry is round.
("Harry" "is" "round" "+")
Harry is smart.
("Harry" "is" "smart" "+")
Harry is young.
("Harry" "is" "young" "+")
If something is kind and smart then it is cold.
((("something" "is" "kind" "+") ("something" "is" "smart" "+")) -> ("something" "is" "cold" "+"))
All young, big things are kind.
((("something" "is" "young" "+") ("something" "is" "big" "+")) -> ("something" "is" "kind" "+"))
Kind things are round.
((("something" "is" "kind" "+")) -> ("something" "is" "round" "+"))
Harry is young.
True
1
proof
[(triple12)]
("Harry" "is" "young" "+")
triple12
Harry is not big.
False
1
inv-proof
[(triple6)]
("Harry" "is" "big" "-")
triple6
Dave is cold.
True
3
proof
[(((triple2 triple3) -> rule1))]
("Dave" "is" "cold" "+")
((triple2 triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is not cold.
False
3
inv-proof
[(((triple2 triple3) -> rule1))]
("Dave" "is" "cold" "-")
((triple2 triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Fiona is round.
True
4
proof
[(((((triple5 triple4) -> rule2)) -> rule3))]
("Fiona" "is" "round" "+")
((((triple5 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not round.
False
4
inv-proof
[(((((triple5 triple4) -> rule2)) -> rule3))]
("Fiona" "is" "round" "-")
((((triple5 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2
Fiona is not cold.
Unknown
inv-rconc
[@1: Fiona is cold.[CWA. Example of deepest failure = (rule1 <- FAIL)]]
("Fiona" "is" "cold" "-")
Dave is young.
Unknown
random
[@0: Dave is young.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "young" "+")
Fiona is not rough.
Unknown
inv-random
[@0: Fiona is rough.[CWA. Example of deepest failure = (FAIL)]]
("Fiona" "is" "rough" "-")
Dave is rough.
Unknown
random
[@0: Dave is rough.[CWA. Example of deepest failure = (FAIL)]]
("Dave" "is" "rough" "+")
@0: Dave is big.[(triple1)] Dave is kind.[(triple2)] Dave is smart.[(triple3)] Fiona is big.[(triple4)] Fiona is young.[(triple5)] Harry is big.[(triple6)] Harry is cold.[(triple7 OR ((triple8 triple11) -> rule1) OR ((((triple12 triple6) -> rule2) triple11) -> rule1))] Harry is kind.[(triple8 OR ((triple12 triple6) -> rule2))] Harry is rough.[(triple9)] Harry is round.[(triple10 OR ((triple8) -> rule3) OR ((((triple12 triple6) -> rule2)) -> rule3))] Harry is smart.[(triple11)] Harry is young.[(triple12)] @1: Dave is cold.[(((triple2 triple3) -> rule1))] Dave is round.[(((triple2) -> rule3))] Fiona is kind.[(((triple5 triple4) -> rule2))] @2: Fiona is round.[(((((triple5 triple4) -> rule2)) -> rule3))]
Dave is big.
("Dave" "is" "big" "+")
triple1
Dave is kind.
("Dave" "is" "kind" "+")
triple2
Dave is smart.
("Dave" "is" "smart" "+")
triple3
Fiona is big.
("Fiona" "is" "big" "+")
triple4
Fiona is young.
("Fiona" "is" "young" "+")
triple5
Harry is big.
("Harry" "is" "big" "+")
triple6
Harry is cold.
("Harry" "is" "cold" "+")
triple7
((triple8 triple11) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
((((triple12 triple6) -> (rule2 % int2)) triple11) -> (rule1 % int1))
Harry is cold.
("Harry" "is" "cold" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is kind.
("Harry" "is" "kind" "+")
triple8
((triple12 triple6) -> (rule2 % int1))
Harry is kind.
("Harry" "is" "kind" "+")
int1
Harry is rough.
("Harry" "is" "rough" "+")
triple9
Harry is round.
("Harry" "is" "round" "+")
triple10
((triple8) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
((((triple12 triple6) -> (rule2 % int2))) -> (rule3 % int1))
Harry is round.
("Harry" "is" "round" "+")
int1
Harry is kind.
("Harry" "is" "kind" "+")
int2
Harry is smart.
("Harry" "is" "smart" "+")
triple11
Harry is young.
("Harry" "is" "young" "+")
triple12
Dave is cold.
("Dave" "is" "cold" "+")
((triple2 triple3) -> (rule1 % int1))
Dave is cold.
("Dave" "is" "cold" "+")
int1
Dave is round.
("Dave" "is" "round" "+")
((triple2) -> (rule3 % int1))
Dave is round.
("Dave" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
((triple5 triple4) -> (rule2 % int1))
Fiona is kind.
("Fiona" "is" "kind" "+")
int1
Fiona is round.
("Fiona" "is" "round" "+")
((((triple5 triple4) -> (rule2 % int2))) -> (rule3 % int1))
Fiona is round.
("Fiona" "is" "round" "+")
int1
Fiona is kind.
("Fiona" "is" "kind" "+")
int2